1  /-
  2  Copyright (c) 2019 Alexander Bentkamp. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Alexander Bentkamp, Yury Kudriashov
  5  -/
  6  
  7  import data.complex.basic
src         └────────────────┘
  8  import data.set.intervals
src         └────────────────┘
  9  import tactic.interactive
src         └────────────────┘
 10  import tactic.linarith
src         └─────────────┘
 11  import linear_algebra.basic
src         └──────────────────┘
 12  import ring_theory.algebra
src         └─────────────────┘
 13  import algebra.pointwise
src         └───────────────┘
 14  
 15  /-!
 16  # Convex sets and functions on real vector spaces
 17  
 18  In a real vector space, we define the following objects and properties.
 19  
 20  * `segment x y` is the closed segment joining `x` and `y`.
 21  * A set `s` is `convex` if for any two points `x y ∈ s` it includes `segment x y`;
 22  * A function `f` is `convex_on` a set `s` if `s` is itself a convex set, and for any two points
 23    `x y ∈ s` the segment joining `(x, f x)` to `(y, f y)` is (non-strictly) above the graph of `f`;
 24    equivalently, `convex_on f s` means that the epigraph `{p : E × ℝ | p.1 ∈ s ∧ f p.1 ≤ p.2}`
 25    is a convex set;
 26  * Center mass of a finite set of points with prescribed weights.
 27  * Convex hull of a set `s` is the minimal convex set that includes `s`.
 28  * Standard simplex `std_simplex ι [fintype ι]` is the intersection of the positive quadrant with
 29    the hyperplane `s.sum = 1` in the space `ι → ℝ`.
 30  
 31  We also provide various equivalent versions of the definitions above, prove that some specific sets
 32  are convex, and prove Jensen's inequality.
 33  
 34  ## Notations
 35  
 36  We use the following local notations:
 37  
 38  * `I = Icc (0:ℝ) 1`;
 39  * `[x, y] = segment x y`.
 40  
 41  They are defined using `local notation`, so they are not available outside of this file.
 42  -/
 43  
 44  universes u' u v w x
 45  
 46  variables {E : Type u} {F : Type v} {ι : Type w} {ι' : Type x}
 47    [add_comm_group E] [vector_space ℝ E] [add_comm_group F] [vector_space ℝ F]
id      └────────────┘     └──────────┘      └────────────┘     └──────────┘ 
src     └────────────┘     └──────────┘      └────────────┘     └──────────┘ 
typ     └────────────┘     └──────────┘      └────────────┘     └──────────┘ 
doc                        └──────────┘                          └──────────┘
 48    {s : set E}
id          └─┘
src         └─┘
typ         └─┘
 49  
 50  open set
 51  open_locale classical
 52  
 53  local notation `I` := (Icc 0 1 : set ℝ)
id                          └─┘       └─┘
src                         └─┘       └─┘
typ                         └─┘       └─┘
doc                         └─┘
 54  
 55  local attribute [instance] set.pointwise_add set.smul_set
id                              └───────────────┘ └──────────┘
src                             └───────────────┘ └──────────┘
typ                             └───────────────┘ └──────────┘
doc                                               └──────────┘
 56  
 57  section sets
 58  
 59  /-! ### Segment -/
 60  
 61  /-- Segments in a vector space -/
 62  def segment (x y : E) : set E :=
id                          └─┘ 
src                          └─┘
typ                         └─┘ 
 63  {z : E | ∃ (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), a • x + b • y = z}
id                                                                
src                                                                       
typ                                                               
 64  local notation `[`x `, ` y `]` := segment x y
id                                     └─────┘
src                                    └─────┘
typ                                    └─────┘
doc                                    └─────┘
 65  
 66  lemma segment_symm (x y : E) : [x, y] = [y, x] :=
id                                     
src                                         
typ                                    
doc                                          
 67  set.ext $ λ z,
id   └─────┘     
src  └─────┘
typ  └─────┘     
 68  ⟨λ ⟨a, b, ha, hb, hab, H⟩, ⟨b, a, hb, ha, (add_comm _ _).trans hab, (add_comm _ _).trans H⟩,
id          └┘  └┘  └─┘                     └──────┘     └───┘        └──────┘     └───┘
src                                             └──────┘     └───┘        └──────┘     └───┘
typ         └┘  └┘  └─┘                     └──────┘     └───┘        └──────┘     └───┘
 69    λ ⟨a, b, ha, hb, hab, H⟩, ⟨b, a, hb, ha, (add_comm _ _).trans hab, (add_comm _ _).trans H⟩⟩
id           └┘  └┘  └─┘                     └──────┘     └───┘        └──────┘     └───┘
src                                              └──────┘     └───┘        └──────┘     └───┘
typ          └┘  └┘  └─┘                     └──────┘     └───┘        └──────┘     └───┘
 70  
 71  lemma left_mem_segment (x y : E) : x ∈ [x, y] :=
id                                        
src                                           
typ                                       
doc                                            
 72  ⟨1, 0, zero_le_one, le_refl 0, add_zero 1, by rw [zero_smul, one_smul, add_zero]⟩
id          └─────────┘  └─────┘    └──────┘           └───────┘  └──────┘  └──────┘
src         └─────────┘  └─────┘    └──────┘       └──┘└───────┘└┘└──────┘└┘└──────┘
typ         └─────────┘  └─────┘    └──────┘       └──┘└───────┘└┘└──────┘└┘└──────┘
doc                                                └──┘         └┘        └┘        
txt                                                └──┘         └┘        └┘        
par                                                └──┘         └┘        └┘        
pid                                                  └┘         └┘        └┘        
st                                                └────────────┘└────────┘└────────┘
 73  
 74  lemma right_mem_segment (x y : E) : y ∈ [x, y] :=
id                                         
src                                            
typ                                        
doc                                             
 75  segment_symm y x ▸ left_mem_segment y x
id   └──────────┘    └──────────────┘  
src  └──────────┘      └──────────────┘
typ  └──────────┘    └──────────────┘  
 76  
 77  lemma segment_same (x : E) : [x, x] = {x} :=
id                                  
src                                    
typ                                 
doc                                  
 78  set.ext $ λ z, ⟨λ ⟨a, b, ha, hb, hab, hz⟩,
id   └─────┘          
src  └─────┘
typ  └─────┘          
 79    by simpa only [(add_smul _ _ _).symm, mem_singleton_iff, hab, one_smul, eq_comm] using hz,
id                     └──────┘              └───────────────┘  └─┘  └──────┘  └─────┘        └┘
src       └──────────┘ └──────┘└────────────┘└───────────────┘└┘   └┘└──────┘└┘└─────┘└──────┘
typ       └──────────┘ └──────┘└────────────┘└───────────────┘└┘└─┘└┘└──────┘└┘└─────┘└──────┘└┘
doc       └──────────┘         └────────────┘                 └┘   └┘        └┘       └──────┘
txt       └──────────┘         └────────────┘                 └┘   └┘        └┘       └──────┘
par       └──────────┘         └────────────┘                 └┘   └┘        └┘       └──────┘
pid            └──┘└┘         └────────────┘                 └┘   └┘        └┘       └────┘
st       └─────────────────────────────────────────────────────────────────────────────────────┘
 80    λ h, mem_singleton_iff.1 h ▸ left_mem_segment z z⟩
id         └───────────────┘    └──────────────┘  
src         └───────────────┘     └──────────────┘
typ        └───────────────┘    └──────────────┘  
 81  
 82  lemma segment_eq_image (x y : E) : segment x y = (λ (θ : ℝ), (1 - θ) • x + θ • y) '' I :=
id                                     └─────┘                            └┘ 
src                                     └─────┘                                  └┘ 
typ                                    └─────┘                            └┘ 
doc                                     └─────┘                                           
 83  set.ext $ λ z,
id   └─────┘     
src  └─────┘
typ  └─────┘     
 84    ⟨λ ⟨a, b, ha, hb, hab, hz⟩,
id             └┘  └┘  └─┘  └┘
typ            └┘  └┘  └─┘  └┘
 85      ⟨b, ⟨hb, hab ▸ le_add_of_nonneg_left ha⟩, hab ▸ hz ▸ by simp only [add_sub_cancel]⟩,
id                     └───────────────────┘                             └────────────┘
src                    └───────────────────┘                  └─────────┘└────────────┘
typ                    └───────────────────┘                  └─────────┘└────────────┘
doc                                                              └─────────┘              
txt                                                              └─────────┘              
par                                                              └─────────┘              
pid                                                                  └──┘└┘              
st                                                              └─────────────────────────┘
 86      λ ⟨θ, ⟨hθ₀, hθ₁⟩, hz⟩, ⟨1-θ, θ, sub_nonneg.2 hθ₁, hθ₀, sub_add_cancel _ _, hz⟩⟩
id            └─┘  └─┘   └┘           └────────┘            └────────────┘
src                                     └────────┘            └────────────┘
typ           └─┘  └─┘   └┘           └────────┘            └────────────┘
 87  
 88  lemma segment_eq_image' (x y : E) : segment x y = (λ (θ : ℝ), x + θ • (y - x)) '' I :=
id                                      └─────┘                         └┘ 
src                                      └─────┘                               └┘ 
typ                                     └─────┘                         └┘ 
doc                                      └─────┘                                       
 89  by { convert segment_eq_image x y, ext θ, simp only [smul_sub, sub_smul, one_smul], abel }
id                └──────────────┘                      └──────┘  └──────┘  └──────┘
src       └──────┘└──────────────┘    └───┘  └─────────┘└──────┘└┘└──────┘└┘└──────┘  └───┘
typ       └──────┘└──────────────┘  └───┘  └─────────┘└──────┘└┘└──────┘└┘└──────┘  └───┘
doc       └──────┘                    └───┘  └─────────┘        └┘        └┘          └───┘
txt       └──────┘                    └───┘  └─────────┘        └┘        └┘          └───┘
par       └──────┘                    └───┘  └─────────┘        └┘        └┘          └───┘
pid                                     └┘      └──┘└┘        └┘        └┘              
st     └─────────────────────────────┘└─────┘└────────────────────────────────────────┘└─────┘└┘
 90  
 91  lemma segment_eq_image₂ (x y : E) :
id                                  
typ                                 
 92    segment x y = (λ p:ℝ×ℝ, p.1 • x + p.2 • y) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} :=
id     └─────┘                     └┘                     
src    └─────┘                           └┘                          
typ    └─────┘                     └┘                     
doc    └─────┘
 93  by simp only [segment, image, prod.exists, mem_set_of_eq, exists_prop, and_assoc]
id                 └─────┘  └───┘  └─────────┘  └───────────┘  └─────────┘  └───────┘
src     └─────────┘└─────┘└┘└───┘└┘└─────────┘└┘└───────────┘└┘└─────────┘└┘└───────┘└─
typ     └─────────┘└─────┘└┘└───┘└┘└─────────┘└┘└───────────┘└┘└─────────┘└┘└───────┘└─
doc     └─────────┘└─────┘└┘     └┘           └┘             └┘           └┘         └─
txt     └─────────┘       └┘     └┘           └┘             └┘           └┘         └─
par     └─────────┘       └┘     └┘           └┘             └┘           └┘         └─
pid         └──┘└┘       └┘     └┘           └┘             └┘           └┘         
st     └───────────────────────────────────────────────────────────────────────────────
 94  
src  
typ  
doc  
txt  
par  
pid  
st   
 95  lemma segment_eq_Icc {a b : ℝ} (h : a ≤ b) : [a, b] = Icc a b :=
id                                               └─┘  
src                                                  └─┘
typ                                              └─┘  
doc                                                     └─┘
 96  begin
st   └─────
 97    rw [segment_eq_image'],
id         └───────────────┘
src    └──┘└───────────────┘
typ    └──┘└───────────────┘
doc    └──┘                 
txt    └──┘                 
par    └──┘                 
pid      └┘                 
st   ──────────────────────┘└──
 98    show (((+) a) ∘ (λ t, t * (b - a))) '' Icc 0 1 = Icc a b,
id                                     └┘          └─┘  
src    └───┘  └─┘ └┘  └──┘    └──┘└┘   └───┘└─┘ 
typ    └───┘  └─┘ └┘  └──┘    └──┘└┘   └───┘└─┘
doc    └───┘   └─┘ └┘   └──┘      └──┘     └───┘ └─┘ 
txt    └───┘   └─┘ └┘   └──┘      └──┘     └───┘     
par    └───┘   └─┘ └┘   └──┘      └──┘     └───┘     
pid    └───┘   └─┘ └┘   └──┘      └──┘     └───┘     
st   ─────────────────────────────────────────────────────────┘└─
 99    rw [image_comp, image_mul_right_Icc (@zero_le_one ℝ _) (sub_nonneg.2 h), image_add_left_Icc],
id         └────────┘  └─────────────────┘   └─────────┘       └────────┘      └────────────────┘
src    └──┘└────────┘└┘└─────────────────┘  └─────────┘ └──┘ └────────┘└─┘ └─┘└────────────────┘
typ    └──┘└────────┘└┘└─────────────────┘  └─────────┘ └──┘ └────────┘└─┘└─┘└────────────────┘
doc    └──┘          └┘                                 └──┘           └─┘ └─┘                  
txt    └──┘          └┘                                 └──┘           └─┘ └─┘                  
par    └──┘          └┘                                 └──┘           └─┘ └─┘                  
pid      └┘          └┘                                 └──┘           └─┘ └─┘                  
st   ───────────────┘└───────────────────────────────────────────────────────┘└──────────────────┘└──
100    simp
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid        
st   ──────┘
101  end
st   └─┘
102  
103  lemma segment_eq_Icc' (a b : ℝ) : [a, b] = Icc (min a b) (max a b) :=
id                                       └─┘  └─┘     └─┘  
src                                        └─┘  └─┘       └─┘
typ                                      └─┘  └─┘     └─┘  
doc                                          └─┘
104  by cases le_total a b; [skip, rw segment_symm]; simp [segment_eq_Icc, *]
id            └──────┘             └──────────┘         └────────────┘
src     └────┘└──────┘    └──┘  └─┘└──────────┘   └────┘└────────────┘└────
typ     └────┘└──────┘  └──┘  └─┘└──────────┘   └────┘└────────────┘└────
doc     └────┘             └──┘  └─┘               └────┘              └────
txt     └────┘             └──┘  └─┘               └────┘              └────
par     └────┘             └──┘  └─┘               └────┘              └────
pid                                                                └──┘
st     └─────────────────────────────┘└──────────┘└───────────────────────────
105  
src  
typ  
doc  
txt  
par  
pid  
st   
106  lemma segment_eq_interval (a b : ℝ) : segment a b = interval a b :=
id                                        └─────┘    └──────┘  
src                                       └─────┘      └──────┘
typ                                       └─────┘    └──────┘  
doc                                        └─────┘       └──────┘
107  segment_eq_Icc' _ _
id   └─────────────┘
src  └─────────────┘
typ  └─────────────┘
108  
109  lemma mem_segment_translate (a : E) {x b c} : a + x ∈ [a + b, a + c] ↔ x ∈ [b, c] :=
id                                                              
src                                                                       
typ                                                             
doc                                                                             
110  begin
st   └─────
111    rw [segment_eq_image', segment_eq_image'],
id         └───────────────┘  └───────────────┘
src    └──┘└───────────────┘└┘└───────────────┘
typ    └──┘└───────────────┘└┘└───────────────┘
doc    └──┘                 └┘                 
txt    └──┘                 └┘                 
par    └──┘                 └┘                 
pid      └┘                 └┘                 
st   ──────────────────────┘└─────────────────┘└──
112    refine exists_congr (λ θ, and_congr iff.rfl _),
id            └──────────┘       └───────┘ └─────┘
src    └─────┘└──────────┘  └──┘└───────┘└─────┘└─┘
typ    └─────┘└──────────┘  └──┘└───────┘└─────┘└─┘
doc    └─────┘              └──┘                └─┘
txt    └─────┘              └──┘                └─┘
par    └─────┘              └──┘                └─┘
pid                        └──┘                └─┘
st   ───────────────────────────────────────────────┘└─
113    simp only [add_sub_add_left_eq_sub, add_assoc, add_left_inj]
id                └─────────────────────┘  └───────┘  └──────────┘
src    └─────────┘└─────────────────────┘└┘└───────┘└┘└──────────┘└┘
typ    └─────────┘└─────────────────────┘└┘└───────┘└┘└──────────┘└┘
doc    └─────────┘                       └┘         └┘            └┘
txt    └─────────┘                       └┘         └┘            └┘
par    └─────────┘                       └┘         └┘            └┘
pid        └──┘└┘                       └┘         └┘            
st   ──────────────────────────────────────────────────────────────┘
114  end
st   └─┘
115  
116  lemma segment_translate_preimage (a b c : E) : (λ x, a + x) ⁻¹' [a + b, a + c] = [b, c] :=
id                                                          └─┘         
src                                                             └─┘               
typ                                                         └─┘         
doc                                                              └─┘                  
117  set.ext $ λ x, mem_segment_translate a
id   └─────┘       └───────────────────┘ 
src  └─────┘        └───────────────────┘
typ  └─────┘       └───────────────────┘ 
118  
119  lemma segment_translate_image (a b c: E) : (λx, a + x) '' [b, c] = [a + b, a + c] :=
id                                                     └┘         
src                                                        └┘               
typ                                                    └┘         
doc                                                                             
120  segment_translate_preimage a b c ▸ image_preimage_eq $ add_left_surjective a
id   └────────────────────────┘     └───────────────┘   └─────────────────┘ 
src  └────────────────────────┘        └───────────────┘   └─────────────────┘
typ  └────────────────────────┘     └───────────────┘   └─────────────────┘ 
121  
122  /-! ### Convexity of sets -/
123  /-- Convexity of sets -/
124  def convex (s : set E) :=
id                   └─┘ 
src                  └─┘
typ                  └─┘ 
125  ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 →
id                                                    
src                                                            
typ                                                   
126    a • x + b • y ∈ s
id             
src               
typ            
127  
128  lemma convex_iff_segment_subset : convex s ↔ ∀ ⦃x y⦄, x ∈ s → y ∈ s → [x, y] ⊆ s :=
id                                     └────┘                       
src                                    └────┘                               
typ                                    └────┘                       
doc                                    └────┘                                 
129  by simp only [convex, segment_eq_image₂, subset_def, ball_image_iff, prod.forall,
id                 └────┘  └───────────────┘  └────────┘  └────────────┘  └─────────┘
src     └─────────┘└────┘└┘└───────────────┘└┘└────────┘└┘└────────────┘└┘└─────────┘└─
typ     └─────────┘└────┘└┘└───────────────┘└┘└────────┘└┘└────────────┘└┘└─────────┘└─
doc     └─────────┘└────┘└┘                 └┘          └┘              └┘           └─
txt     └─────────┘      └┘                 └┘          └┘              └┘           └─
par     └─────────┘      └┘                 └┘          └┘              └┘           └─
pid         └──┘└┘      └┘                 └┘          └┘              └┘           └─
st     └───────────────────────────────────────────────────────────────────────────────
130    mem_set_of_eq, and_imp]
id     └───────────┘  └─────┘
src  ─┘└───────────┘└┘└─────┘└─
typ  ─┘└───────────┘└┘└─────┘└─
doc  ─┘             └┘       └─
txt  ─┘             └┘       └─
par  ─┘             └┘       └─
pid  ─┘             └┘       
st   ──────────────────────────
131  
src  
typ  
doc  
txt  
par  
pid  
st   
132  lemma convex.segment_subset (h : convex s) {x y:E} (hx : x ∈ s) (hy : y ∈ s) : [x, y] ⊆ s :=
id                                    └────┘                                   
src                                   └────┘                                          
typ                                   └────┘                                   
doc                                   └────┘                                           
133  convex_iff_segment_subset.1 h hx hy
id   └───────────────────────┘   └┘ └┘
src  └───────────────────────┘
typ  └───────────────────────┘   └┘ └┘
134  
135  /-- Alternative definition of set convexity, in terms of pointwise set operations. -/
136  lemma convex_iff_pointwise_add_subset:
137    convex s ↔ ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • s + b • s ⊆ s :=
id     └────┘                                           
src    └────┘                                                   
typ    └────┘                                           
doc    └────┘
138  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
139    begin
st     └─────
140      rintros hA a b ha hb hab w ⟨au, ⟨u, hu, rfl⟩, bv, ⟨v, hv, rfl⟩, rfl⟩,
src      └──────────────────────────────────────────────────────────────────┘
typ      └──────────────────────────────────────────────────────────────────┘
doc      └──────────────────────────────────────────────────────────────────┘
txt      └──────────────────────────────────────────────────────────────────┘
par      └──────────────────────────────────────────────────────────────────┘
pid             └───────────────────────────────────────────────────────────┘
st   ───────────────────────────────────────────────────────────────────────┘└─
141      exact hA hu hv ha hb hab
id             └┘ └┘ └┘ └┘ └┘ └─┘
src      └────┘             
typ      └────┘└┘└┘└┘└┘└┘└─┘
doc      └────┘             
txt      └────┘             
par      └────┘             
pid                        
st   ─────────────────────────────
142    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
143    (λ h x y hx hy a b ha hb hab,
id           └┘ └┘   └┘ └┘ └─┘
typ          └┘ └┘   └┘ └┘ └─┘
144      (h ha hb hab) (set.add_mem_pointwise_add ⟨_, hx, rfl⟩ ⟨_, hy, rfl⟩))
id         └┘ └┘ └─┘   └───────────────────────┘     └┘  └─┘      └┘  └─┘
src                     └───────────────────────┘         └─┘          └─┘
typ        └┘ └┘ └─┘   └───────────────────────┘     └┘  └─┘      └┘  └─┘
145  
146  /-- Alternative definition of set convexity, using division -/
147  lemma convex_iff_div:
148    convex s ↔ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : ℝ⦄,
id     └────┘                                  
src    └────┘                                        
typ    └────┘                                  
doc    └────┘
149      0 ≤ a → 0 ≤ b → 0 < a + b → (a/(a+b)) • x + (b/(a+b)) • y ∈ s :=
id                                           
src                                                     
typ                                          
150  ⟨begin
st    └─────
151    assume h x y hx hy a b ha hb hab,
src    └──────────────────────────────┘
typ    └──────────────────────────────┘
doc    └──────────────────────────────┘
txt    └──────────────────────────────┘
par    └──────────────────────────────┘
pid    └──────────────────────────────┘
st   ─────────────────────────────────┘└─
152    apply h hx hy,
id            └┘ └┘
src    └────┘   
typ    └────┘└┘└┘
doc    └────┘   
txt    └────┘   
par    └────┘   
pid            
st   ──────────────┘└─
153    have ha', from mul_le_mul_of_nonneg_left ha (le_of_lt (inv_pos hab)),
id                    └───────────────────────┘ └┘  └──────┘  └─────┘ └─┘
src    └──────┘  └───┘└───────────────────────┘   └──────┘ └─────┘   └┘
typ    └──────┘  └───┘└───────────────────────┘└┘ └──────┘ └─────┘└─┘└┘
doc    └──────┘  └───┘                                               └┘
txt    └──────┘  └───┘                                               └┘
par    └──────┘  └───┘                                               └┘
pid    └──────┘  └───┘                                               └┘
st   ─────────┘└──────────────────────────────────────────────────────────┘└─
154    rwa [mul_zero, ←div_eq_inv_mul] at ha',
id          └──────┘   └────────────┘
src    └───┘└──────┘└─┘└────────────┘└──────┘
typ    └───┘└──────┘└─┘└────────────┘└──────┘
doc    └───┘        └─┘              └──────┘
txt    └───┘        └─┘              └──────┘
par    └───┘        └─┘              └──────┘
pid       └┘        └─┘              └─────┘
st   ──────────────┘└───────────────┘└─────┘└─
155    have hb', from mul_le_mul_of_nonneg_left hb (le_of_lt (inv_pos hab)),
id                    └───────────────────────┘ └┘  └──────┘  └─────┘ └─┘
src    └──────┘  └───┘└───────────────────────┘   └──────┘ └─────┘   └┘
typ    └──────┘  └───┘└───────────────────────┘└┘ └──────┘ └─────┘└─┘└┘
doc    └──────┘  └───┘                                               └┘
txt    └──────┘  └───┘                                               └┘
par    └──────┘  └───┘                                               └┘
pid    └──────┘  └───┘                                               └┘
st   ─────────┘└──────────────────────────────────────────────────────────┘└─
156    rwa [mul_zero, ←div_eq_inv_mul] at hb',
id          └──────┘   └────────────┘
src    └───┘└──────┘└─┘└────────────┘└──────┘
typ    └───┘└──────┘└─┘└────────────┘└──────┘
doc    └───┘        └─┘              └──────┘
txt    └───┘        └─┘              └──────┘
par    └───┘        └─┘              └──────┘
pid       └┘        └─┘              └─────┘
st   ──────────────┘└───────────────┘└─────┘└─
157    rw [←add_div],
id          └─────┘
src    └───┘└─────┘
typ    └───┘└─────┘
doc    └───┘       
txt    └───┘       
par    └───┘       
pid      └─┘       
st   ─────────────┘└──
158    exact div_self (ne_of_lt hab).symm
id           └──────┘  └──────┘ └─┘
src    └────┘└──────┘ └──────┘   └─────┘
typ    └────┘└──────┘ └──────┘└─┘└─────┘
doc    └────┘                    └─────┘
txt    └────┘                    └─────┘
par    └────┘                    └─────┘
pid                             └───┘└┘
st   ────────────────────────────────────┘
159  end,
st   └─┘
160  begin
st   └─────
161    assume h x y hx hy a b ha hb hab,
src    └──────────────────────────────┘
typ    └──────────────────────────────┘
doc    └──────────────────────────────┘
txt    └──────────────────────────────┘
par    └──────────────────────────────┘
pid    └──────────────────────────────┘
st   ─────────────────────────────────┘└─
162    have h', from h hx hy ha hb,
id                    └┘ └┘ └┘ └┘
src    └─────┘  └───┘       
typ    └─────┘  └───┘└┘└┘└┘└┘
doc    └─────┘  └───┘       
txt    └─────┘  └───┘       
par    └─────┘  └───┘       
pid    └─────┘  └───┘       
st   ────────┘└──────────────────┘└─
163    rw [hab, div_one, div_one] at h',
id         └─┘  └─────┘  └─────┘
src    └──┘   └┘└─────┘└┘└─────┘└─────┘
typ    └──┘└─┘└┘└─────┘└┘└─────┘└─────┘
doc    └──┘   └┘       └┘       └─────┘
txt    └──┘   └┘       └┘       └─────┘
par    └──┘   └┘       └┘       └─────┘
pid      └┘   └┘       └┘       └────┘
st   ────────┘└───────┘└───────┘└────┘└─
164    exact h' zero_lt_one
id           └┘ └─────────┘
src    └────┘  └─────────┘
typ    └────┘└┘└─────────┘
doc    └────┘             
txt    └────┘             
par    └────┘             
pid                      
st   ──────────────────────┘
165  end⟩
st   └─┘
166  
167  /-! ### Examples of convex sets -/
168  
169  lemma convex_empty : convex (∅ : set E) :=  by finish
id                        └────┘     └─┘ 
src                       └────┘     └─┘           └──────
typ                       └────┘     └─┘          └──────
doc                       └────┘                    └──────
txt                                                 └──────
par                                                 └──────
pid                                                       
st                                                 └───────
170  
src  
typ  
doc  
txt  
par  
pid  
st   
171  lemma convex_singleton (c : E) : convex ({c} : set E) :=
id                                   └────┘      └─┘ 
src                                   └────┘       └─┘
typ                                  └────┘      └─┘ 
doc                                   └────┘
172  begin
st   └─────
173    intros x y hx hy a b ha hb hab,
src    └────────────────────────────┘
typ    └────────────────────────────┘
doc    └────────────────────────────┘
txt    └────────────────────────────┘
par    └────────────────────────────┘
pid          └──────────────────────┘
st   ───────────────────────────────┘└─
174    rw [set.eq_of_mem_singleton hx, set.eq_of_mem_singleton hy, ←add_smul, hab, one_smul],
id         └─────────────────────┘ └┘  └─────────────────────┘ └┘   └──────┘  └─┘  └──────┘
src    └──┘└─────────────────────┘  └┘└─────────────────────┘  └─┘└──────┘└┘   └┘└──────┘
typ    └──┘└─────────────────────┘└┘└┘└─────────────────────┘└┘└─┘└──────┘└┘└─┘└┘└──────┘
doc    └──┘                         └┘                         └─┘        └┘   └┘        
txt    └──┘                         └┘                         └─┘        └┘   └┘        
par    └──┘                         └┘                         └─┘        └┘   └┘        
pid      └┘                         └┘                         └─┘        └┘   └┘        
st   ───────────────────────────────┘└──────────────────────────┘└─────────┘└───┘└────────┘└──
175    exact mem_singleton c
id           └───────────┘ 
src    └────┘└───────────┘ 
typ    └────┘└───────────┘
doc    └────┘              
txt    └────┘              
par    └────┘              
pid                       
st   ───────────────────────┘
176  end
st   └─┘
177  
178  lemma convex_univ : convex (set.univ : set E) := λ _ _ _ _ _ _ _ _ _, trivial
id                       └────┘  └──────┘   └─┘                  └─────┘
src                      └────┘  └──────┘   └─┘                            └─────┘
typ                      └────┘  └──────┘   └─┘                  └─────┘
doc                      └────┘
179  
180  lemma convex.inter {t : set E} (hs: convex s) (ht: convex t) : convex (s ∩ t) :=
id                           └─┘        └────┘        └────┘     └────┘    
src                          └─┘         └────┘         └────┘      └────┘    
typ                          └─┘        └────┘        └────┘     └────┘    
doc                                      └────┘         └────┘      └────┘
181  λ x y (hx : x ∈ s ∩ t) (hy : y ∈ s ∩ t) a b (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1),
id                                                                 
src                                                                              
typ                                                                
182    ⟨hs hx.left hy.left ha hb hab, ht hx.right hy.right ha hb hab⟩
id      └┘ └┘└───┘ └┘└───┘ └┘ └┘ └─┘  └┘ └┘└────┘ └┘└────┘ └┘ └┘ └─┘
src          └───┘   └───┘                 └────┘   └────┘
typ     └┘ └┘└───┘ └┘└───┘ └┘ └┘ └─┘  └┘ └┘└────┘ └┘└────┘ └┘ └┘ └─┘
183  
184  lemma convex_sInter {S : set (set E)} (h : ∀ s ∈ S, convex s) : convex (⋂₀ S) :=
id                            └─┘  └─┘                └────┘     └────┘  └┘ 
src                           └─┘  └─┘                  └────┘      └────┘  └┘
typ                           └─┘  └─┘                └────┘     └────┘  └┘ 
doc                                                      └────┘      └────┘  └┘
185  assume x y hx hy a b ha hb hab s hs,
id            └┘ └┘   └┘ └┘ └─┘  └┘
typ           └┘ └┘   └┘ └┘ └─┘  └┘
186  h s hs (hx s hs) (hy s hs) ha hb hab
id     └┘  └┘  └┘   └┘  └┘  └┘ └┘ └─┘
typ    └┘  └┘  └┘   └┘  └┘  └┘ └┘ └─┘
187  
188  lemma convex_Inter {ι : Sort*} {s: ι → set E} (h: ∀ i : ι, convex (s i)) : convex (⋂ i, s i) :=
id                                         └─┘               └────┘        └────┘     
src                                         └─┘                 └────┘          └────┘    
typ                                        └─┘               └────┘        └────┘     
doc                                                             └────┘          └────┘    
189  (sInter_range s) ▸ convex_sInter $ forall_range_iff.2 h
id    └──────────┘    └───────────┘   └──────────────┘  
src   └──────────┘     └───────────┘   └──────────────┘
typ   └──────────┘    └───────────┘   └──────────────┘  
190  
191  lemma convex.prod {s : set E} {t : set F} (hs : convex s) (ht : convex t) :
id                          └─┘        └─┘         └────┘         └────┘ 
src                         └─┘         └─┘          └────┘          └────┘
typ                         └─┘        └─┘         └────┘         └────┘ 
doc                                                  └────┘          └────┘
192    convex (s.prod t) :=
id     └────┘  └───┘ 
src    └────┘   └───┘
typ    └────┘  └───┘ 
doc    └────┘   └───┘
193  begin
st   └─────
194    intros x y hx hy a b ha hb hab,
src    └────────────────────────────┘
typ    └────────────────────────────┘
doc    └────────────────────────────┘
txt    └────────────────────────────┘
par    └────────────────────────────┘
pid          └──────────────────────┘
st   ───────────────────────────────┘└─
195    apply mem_prod.2,
id           └──────┘
src    └────┘└──────┘└┘
typ    └────┘└──────┘└┘
doc    └────┘        └┘
txt    └────┘        └┘
par    └────┘        └┘
pid                 └┘
st   ─────────────────┘└─
196    exact ⟨hs (mem_prod.1 hx).1 (mem_prod.1 hy).1 ha hb hab,
id            └┘
src    └────┘            └─┘  └──┘         └─┘  └──┘       └─
typ    └────┘ └┘         └─┘  └──┘         └─┘  └──┘       └─
doc    └────┘            └─┘  └──┘         └─┘  └──┘       └─
txt    └────┘            └─┘  └──┘         └─┘  └──┘       └─
par    └────┘            └─┘  └──┘         └─┘  └──┘       └─
pid                     └─┘  └──┘         └─┘  └──┘       └─
st   ───────────────────────────────────────────────────────────
197          ht (mem_prod.1 hx).2 (mem_prod.1 hy).2 ha hb hab⟩
id           └┘             └┘     └──────┘   └┘    └┘ └┘ └─┘
src  ───────┘           └─┘  └──┘ └──────┘└─┘  └──┘       └┘
typ  ───────┘└┘         └─┘└┘└──┘ └──────┘└─┘└┘└──┘└┘└┘└─┘└┘
doc  ───────┘           └─┘  └──┘         └─┘  └──┘       └┘
txt  ───────┘           └─┘  └──┘         └─┘  └──┘       └┘
par  ───────┘           └─┘  └──┘         └─┘  └──┘       └┘
pid  ───────┘           └─┘  └──┘         └─┘  └──┘       
st   ─────────────────────────────────────────────────────────┘
198  end
st   └─┘
199  
200  lemma convex.is_linear_image (hs : convex s) {f : E → F} (hf : is_linear_map ℝ f) :
id                                      └────┘                   └───────────┘  
src                                     └────┘                      └───────────┘ 
typ                                     └────┘                   └───────────┘  
doc                                     └────┘
201    convex (f '' s) :=
id     └────┘   └┘ 
src    └────┘    └┘
typ    └────┘   └┘ 
doc    └────┘
202  begin
st   └─────
203    rintros _ _ ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩ a b ha hb hab,
src    └─────────────────────────────────────────────────┘
typ    └─────────────────────────────────────────────────┘
doc    └─────────────────────────────────────────────────┘
txt    └─────────────────────────────────────────────────┘
par    └─────────────────────────────────────────────────┘
pid           └──────────────────────────────────────────┘
st   ────────────────────────────────────────────────────┘└─
204    exact ⟨a • x + b • y, hs hx hy ha hb hab, by simp only [hf.add,hf.smul]⟩
id                     └┘ └┘ └┘ └┘ └┘ └─┘
src    └────┘      └┘             └┘  └─────────┘             └┘
typ    └────┘  └┘└┘└┘└┘└┘└┘└─┘└┘  └─────────┘└────┘└─────┘└┘
doc    └────┘        └┘             └┘  └─────────┘             └┘
txt    └────┘        └┘             └┘  └─────────┘             └┘
par    └────┘        └┘             └┘  └─────────┘             └┘
pid                 └┘             └┘  └──────────┘             └┘
st   ─────────────────────────────────────────────┘└─────────────────────────┘└┘
205  end
st   └─┘
206  
207  lemma convex.linear_image (hs : convex s) (f : E →ₗ[ℝ] F) : convex (image f s) :=
id                                   └────┘         └─┘     └────┘  └───┘  
src                                  └────┘           └─┘      └────┘  └───┘
typ                                  └────┘         └─┘     └────┘  └───┘  
doc                                  └────┘                      └────┘
208  hs.is_linear_image f.is_linear
id   └┘└──────────────┘ └────────┘
src    └──────────────┘  └────────┘
typ  └┘└──────────────┘ └────────┘
209  
210  lemma convex.is_linear_preimage {s : set F} (hs : convex s) {f : E → F} (hf : is_linear_map ℝ f) :
id                                        └─┘         └────┘                   └───────────┘  
src                                       └─┘          └────┘                      └───────────┘ 
typ                                       └─┘         └────┘                   └───────────┘  
doc                                                    └────┘
211    convex (preimage f s) :=
id     └────┘  └──────┘  
src    └────┘  └──────┘
typ    └────┘  └──────┘  
doc    └────┘  └──────┘
212  begin
st   └─────
213    intros x y hx hy a b ha hb hab,
src    └────────────────────────────┘
typ    └────────────────────────────┘
doc    └────────────────────────────┘
txt    └────────────────────────────┘
par    └────────────────────────────┘
pid          └──────────────────────┘
st   ───────────────────────────────┘└─
214    convert hs hx hy ha hb hab,
id             └┘ └┘ └┘ └┘ └┘ └─┘
src    └──────┘          
typ    └──────┘└┘└┘└┘└┘└┘└─┘
doc    └──────┘          
txt    └──────┘          
par    └──────┘          
pid                     
st   ───────────────────────────┘└─
215    simp only [mem_preimage, hf.add, hf.smul]
id                └──────────┘
src    └─────────┘└──────────┘└┘      └┘       └┘
typ    └─────────┘└──────────┘└┘└────┘└┘└─────┘└┘
doc    └─────────┘            └┘      └┘       └┘
txt    └─────────┘            └┘      └┘       └┘
par    └─────────┘            └┘      └┘       └┘
pid        └──┘└┘            └┘      └┘       
st   ───────────────────────────────────────────┘
216  end
st   └─┘
217  
218  lemma convex.linear_preimage {s : set F} (hs : convex s) (f : E →ₗ[ℝ] F) :
id                                     └─┘         └────┘         └─┘ 
src                                    └─┘          └────┘           └─┘
typ                                    └─┘         └────┘         └─┘ 
doc                                                 └────┘
219    convex (preimage f s) :=
id     └────┘  └──────┘  
src    └────┘  └──────┘
typ    └────┘  └──────┘  
doc    └────┘  └──────┘
220  hs.is_linear_preimage f.is_linear
id   └┘└─────────────────┘ └────────┘
src    └─────────────────┘  └────────┘
typ  └┘└─────────────────┘ └────────┘
221  
222  lemma convex.neg (hs : convex s) : convex ((λ z, -z) '' s) :=
id                          └────┘     └────┘         └┘ 
src                         └────┘      └────┘           └┘
typ                         └────┘     └────┘         └┘ 
doc                         └────┘      └────┘
223  hs.is_linear_image is_linear_map.is_linear_map_neg
id   └┘└──────────────┘ └─────────────────────────────┘
src    └──────────────┘ └─────────────────────────────┘
typ  └┘└──────────────┘ └─────────────────────────────┘
224  
225  lemma convex.neg_preimage (hs : convex s) : convex ((λ z, -z) ⁻¹' s) :=
id                                   └────┘     └────┘         └─┘ 
src                                  └────┘      └────┘           └─┘
typ                                  └────┘     └────┘         └─┘ 
doc                                  └────┘      └────┘            └─┘
226  hs.is_linear_preimage is_linear_map.is_linear_map_neg
id   └┘└─────────────────┘ └─────────────────────────────┘
src    └─────────────────┘ └─────────────────────────────┘
typ  └┘└─────────────────┘ └─────────────────────────────┘
227  
228  lemma convex.smul (c : ℝ) (hs : convex s) : convex (c • s) :=
id                                  └────┘     └────┘    
src                                 └────┘      └────┘    
typ                                 └────┘     └────┘    
doc                                  └────┘      └────┘
229  begin
st   └─────
230    rw smul_set_eq_image,
id        └───────────────┘
src    └─┘└───────────────┘
typ    └─┘└───────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ─────────────────────┘└─
231    exact hs.is_linear_image (is_linear_map.is_linear_map_smul c)
id           └────────────────┘  └──────────────────────────────┘ 
src    └────┘└────────────────┘ └──────────────────────────────┘ └┘
typ    └────┘└────────────────┘ └──────────────────────────────┘└┘
doc    └────┘                                                    └┘
txt    └────┘                                                    └┘
par    └────┘                                                    └┘
pid                                                             
st   ───────────────────────────────────────────────────────────────┘
232  end
st   └─┘
233  
234  lemma convex.smul_preimage (c : ℝ) (hs : convex s) : convex ((λ z, c • z) ⁻¹' s) :=
id                                           └────┘     └────┘           └─┘ 
src                                          └────┘      └────┘              └─┘
typ                                          └────┘     └────┘           └─┘ 
doc                                           └────┘      └────┘               └─┘
235  hs.is_linear_preimage (is_linear_map.is_linear_map_smul c)
id   └┘└─────────────────┘  └──────────────────────────────┘ 
src    └─────────────────┘  └──────────────────────────────┘
typ  └┘└─────────────────┘  └──────────────────────────────┘ 
236  
237  lemma convex.add {t : set E}  (hs : convex s) (ht : convex t) : convex (s + t) :=
id                         └─┘          └────┘         └────┘     └────┘    
src                        └─┘           └────┘          └────┘      └────┘    
typ                        └─┘          └────┘         └────┘     └────┘    
doc                                      └────┘          └────┘      └────┘
238  by { rw pointwise_add_eq_image, exact (hs.prod ht).is_linear_image is_linear_map.is_linear_map_add }
id           └────────────────────┘         └─────┘ └┘                  └─────────────────────────────┘
src       └─┘└────────────────────┘  └────┘ └─────┘  └────────────────┘└─────────────────────────────┘
typ       └─┘└────────────────────┘  └────┘ └─────┘└┘└────────────────┘└─────────────────────────────┘
doc       └─┘                        └────┘          └────────────────┘                               
txt       └─┘                        └────┘          └────────────────┘                               
par       └─┘                        └────┘          └────────────────┘                               
pid                                                └────────────────┘                               
st     └──────────────────────────┘└───────────────────────────────────────────────────────────────────┘└┘
239  
240  lemma convex.sub {t : set E}  (hs : convex s) (ht : convex t) :
id                         └─┘          └────┘         └────┘ 
src                        └─┘           └────┘          └────┘
typ                        └─┘          └────┘         └────┘ 
doc                                      └────┘          └────┘
241    convex ((λx : E × E, x.1 - x.2) '' (s.prod t)) :=
id     └────┘                  └┘  └───┘ 
src    └────┘                      └┘   └───┘
typ    └────┘                  └┘  └───┘ 
doc    └────┘                               └───┘
242  (hs.prod ht).is_linear_image is_linear_map.is_linear_map_sub
id    └┘└───┘ └┘ └─────────────┘  └─────────────────────────────┘
src     └───┘    └─────────────┘  └─────────────────────────────┘
typ   └┘└───┘ └┘ └─────────────┘  └─────────────────────────────┘
243  
244  lemma convex.translate (hs : convex s) (z : E) : convex ((λx, z + x) '' s) :=
id                                └────┘            └────┘          └┘ 
src                               └────┘              └────┘             └┘
typ                               └────┘            └────┘          └┘ 
doc                               └────┘              └────┘
245  begin
st   └─────
246    convert (convex_singleton z).add hs,
id              └──────────────┘       └┘
src    └──────┘ └──────────────┘ └────┘
typ    └──────┘ └──────────────┘└────┘└┘
doc    └──────┘                  └────┘
txt    └──────┘                  └────┘
par    └──────┘                  └────┘
pid                             └────┘
st   ────────────────────────────────────┘└─
247    ext x,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid       └┘
st   ──────┘└─
248    simp [set.mem_image, mem_pointwise_add, eq_comm]
id           └───────────┘  └───────────────┘  └─────┘
src    └────┘└───────────┘└┘└───────────────┘└┘└─────┘└┘
typ    └────┘└───────────┘└┘└───────────────┘└┘└─────┘└┘
doc    └────┘             └┘                 └┘       └┘
txt    └────┘             └┘                 └┘       └┘
par    └────┘             └┘                 └┘       └┘
pid                     └┘                 └┘       
st   ──────────────────────────────────────────────────┘
249  end
st   └─┘
250  
251  lemma convex.affinity (hs : convex s) (z : E) (c : ℝ) : convex ((λx, z + c • x) '' s) :=
id                               └────┘                   └────┘            └┘ 
src                              └────┘                     └────┘                └┘
typ                              └────┘                   └────┘            └┘ 
doc                              └────┘                      └────┘
252  begin
st   └─────
253    convert (hs.smul c).translate z using 1,
id              └─────┘             
src    └──────┘ └─────┘ └──────────┘ └──────┘
typ    └──────┘ └─────┘└──────────┘└──────┘
doc    └──────┘         └──────────┘ └──────┘
txt    └──────┘         └──────────┘ └──────┘
par    └──────┘         └──────────┘ └──────┘
pid                    └──────────┘ └─────┘
st   ────────────────────────────────────────┘└─
254    erw [smul_set_eq_image, ←image_comp]
id          └───────────────┘   └────────┘
src    └───┘└───────────────┘└─┘└────────┘└┘
typ    └───┘└───────────────┘└─┘└────────┘└┘
doc    └───┘                 └─┘          └┘
txt    └───┘                 └─┘          └┘
par    └───┘                 └─┘          └┘
pid       └┘                 └─┘          
st   ───────────────────────┘└───────────┘
255  end
st   └─┘
256  
257  lemma convex_real_iff {s : set ℝ} :
id                              └─┘ 
src                             └─┘ 
typ                             └─┘ 
258    convex s ↔ ∀ {x y}, x ∈ s → y ∈ s → Icc x y ⊆ s :=
id     └────┘                    └─┘    
src    └────┘                           └─┘     
typ    └────┘                    └─┘    
doc    └────┘                              └─┘
259  begin
st   └─────
260    simp only [convex_iff_segment_subset, segment_eq_Icc'],
id                └───────────────────────┘  └─────────────┘
src    └─────────┘└───────────────────────┘└┘└─────────────┘
typ    └─────────┘└───────────────────────┘└┘└─────────────┘
doc    └─────────┘                         └┘               
txt    └─────────┘                         └┘               
par    └─────────┘                         └┘               
pid        └──┘└┘                         └┘               
st   ───────────────────────────────────────────────────────┘└─
261    split; intros h x y hx hy,
src    └───┘  └────────────────┘
typ    └───┘  └────────────────┘
doc    └───┘  └────────────────┘
txt    └───┘  └────────────────┘
par    └───┘  └────────────────┘
pid                 └──────────┘
st   ──────────────────────────┘└─
262    { cases le_or_lt x y with hxy hxy,
id             └──────┘  
src      └────┘└──────┘  └───────────┘
typ      └────┘└──────┘└───────────┘
doc      └────┘          └───────────┘
txt      └────┘          └───────────┘
par      └────┘          └───────────┘
pid                     └───────────┘
st   ───┘└─────────────────────────────┘└─
263      { simpa [hxy] using h hx hy },
id                └─┘         └┘ └┘
src        └─────┘   └──────┘     
typ        └─────┘└─┘└──────┘└┘└┘
doc        └─────┘   └──────┘     
txt        └─────┘   └──────┘     
par        └─────┘   └──────┘     
pid                └────┘     
st   ─────┘└────────────────────────┘└┘
264      { simp [hxy] } },
id               └─┘
src        └────┘   └┘
typ        └────┘└─┘└┘
doc        └────┘   └┘
txt        └────┘   └┘
par        └────┘   └┘
pid               
st   ────────────────┘└──┘
265    { apply h; cases le_total x y; simp [*] }
id                      └──────┘  
src      └────┘   └────┘└──────┘    └───────┘
typ      └────┘   └────┘└──────┘  └───────┘
doc      └────┘   └────┘            └───────┘
txt      └────┘   └────┘            └───────┘
par      └────┘   └────┘            └───────┘
pid                                   └─┘
st   ─────────────────────────────────────────┘└─
266  end
st   ──┘
267  
268  lemma convex_Iio (r : ℝ) : convex (Iio r) :=
id                             └────┘  └─┘ 
src                            └────┘  └─┘
typ                            └────┘  └─┘ 
doc                             └────┘  └─┘
269  convex_real_iff.2 $ λ x y hx hy z hz, lt_of_le_of_lt hz.2 hy
id   └─────────────┘        └┘ └┘  └┘  └────────────┘ └┘  └┘
src  └─────────────┘                      └────────────┘   
typ  └─────────────┘        └┘ └┘  └┘  └────────────┘ └┘  └┘
270  
271  lemma convex_Ioi (r : ℝ) : convex (Ioi r) :=
id                             └────┘  └─┘ 
src                            └────┘  └─┘
typ                            └────┘  └─┘ 
doc                             └────┘  └─┘
272  convex_real_iff.2 $ λ x y hx hy z hz, lt_of_lt_of_le hx hz.1
id   └─────────────┘        └┘ └┘  └┘  └────────────┘ └┘ └┘
src  └─────────────┘                      └────────────┘      
typ  └─────────────┘        └┘ └┘  └┘  └────────────┘ └┘ └┘
273  
274  lemma convex_Iic (r : ℝ) : convex (Iic r) :=
id                             └────┘  └─┘ 
src                            └────┘  └─┘
typ                            └────┘  └─┘ 
doc                             └────┘  └─┘
275  convex_real_iff.2 $ λ x y hx hy z hz, le_trans hz.2 hy
id   └─────────────┘        └┘ └┘  └┘  └──────┘ └┘  └┘
src  └─────────────┘                      └──────┘   
typ  └─────────────┘        └┘ └┘  └┘  └──────┘ └┘  └┘
276  
277  lemma convex_Ici (r : ℝ) : convex (Ici r) :=
id                             └────┘  └─┘ 
src                            └────┘  └─┘
typ                            └────┘  └─┘ 
doc                             └────┘  └─┘
278  convex_real_iff.2 $ λ x y hx hy z hz, le_trans hx hz.1
id   └─────────────┘        └┘ └┘  └┘  └──────┘ └┘ └┘
src  └─────────────┘                      └──────┘      
typ  └─────────────┘        └┘ └┘  └┘  └──────┘ └┘ └┘
279  
280  lemma convex_Ioo (r : ℝ) (s : ℝ) : convex (Ioo r s) :=
id                                    └────┘  └─┘  
src                                   └────┘  └─┘
typ                                   └────┘  └─┘  
doc                                     └────┘  └─┘
281  (convex_Ioi _).inter (convex_Iio _)
id    └────────┘   └───┘   └────────┘
src   └────────┘   └───┘   └────────┘
typ   └────────┘   └───┘   └────────┘
282  
283  lemma convex_Ico (r : ℝ) (s : ℝ) : convex (Ico r s) :=
id                                    └────┘  └─┘  
src                                   └────┘  └─┘
typ                                   └────┘  └─┘  
doc                                     └────┘  └─┘
284  (convex_Ici _).inter (convex_Iio _)
id    └────────┘   └───┘   └────────┘
src   └────────┘   └───┘   └────────┘
typ   └────────┘   └───┘   └────────┘
285  
286  lemma convex_Ioc (r : ℝ) (s : ℝ) : convex (Ioc r s) :=
id                                    └────┘  └─┘  
src                                   └────┘  └─┘
typ                                   └────┘  └─┘  
doc                                     └────┘  └─┘
287  (convex_Ioi _).inter (convex_Iic _)
id    └────────┘   └───┘   └────────┘
src   └────────┘   └───┘   └────────┘
typ   └────────┘   └───┘   └────────┘
288  
289  lemma convex_Icc (r : ℝ) (s : ℝ) : convex (Icc r s) :=
id                                    └────┘  └─┘  
src                                   └────┘  └─┘
typ                                   └────┘  └─┘  
doc                                     └────┘  └─┘
290  (convex_Ici _).inter (convex_Iic _)
id    └────────┘   └───┘   └────────┘
src   └────────┘   └───┘   └────────┘
typ   └────────┘   └───┘   └────────┘
291  
292  lemma convex_segment (a b : E) : convex [a, b] :=
id                                   └────┘  
src                                   └────┘    
typ                                  └────┘  
doc                                   └────┘    
293  begin
st   └─────
294    have : (λ (t : ℝ), a + t • (b - a)) = (λz : E, a + z) ∘ (λt:ℝ, t • (b - a)) := rfl,
id                                                                            └─┘
src    └─────┘  └────┘ └─┘     └─┘  └──┘ └┘   └┘  └┘ └┘      └────┘└─┘
typ    └─────┘  └────┘ └─┘     └─┘  └──┘└┘   └┘  └┘ └┘    └────┘└─┘
doc    └─────┘  └────┘ └─┘        └─┘   └──┘ └┘   └┘   └┘ └┘      └────┘
txt    └─────┘  └────┘ └─┘        └─┘   └──┘ └┘   └┘   └┘ └┘      └────┘
par    └─────┘  └────┘ └─┘        └─┘   └──┘ └┘   └┘   └┘ └┘      └────┘
pid    └───┘└┘  └────┘ └─┘        └─┘   └──┘ └┘   └┘   └┘ └┘      └┘└──┘
st   ───────────────────────────────────────────────────────────────────────────────────┘└─
295    rw [segment_eq_image', this, image_comp],
id         └───────────────┘  └──┘  └────────┘
src    └──┘└───────────────┘└┘    └┘└────────┘
typ    └──┘└───────────────┘└┘└──┘└┘└────────┘
doc    └──┘                 └┘    └┘          
txt    └──┘                 └┘    └┘          
par    └──┘                 └┘    └┘          
pid      └┘                 └┘    └┘          
st   ──────────────────────┘└────┘└──────────┘└──
296    refine ((convex_Icc _ _).is_linear_image _).translate _,
id              └────────┘
src    └─────┘  └────────┘└──────────────────────────────────┘
typ    └─────┘  └────────┘└──────────────────────────────────┘
doc    └─────┘            └──────────────────────────────────┘
txt    └─────┘            └──────────────────────────────────┘
par    └─────┘            └──────────────────────────────────┘
pid                      └──────────────────────────────────┘
st   ────────────────────────────────────────────────────────┘└─
297    exact is_linear_map.is_linear_map_smul' _
id           └───────────────────────────────┘
src    └────┘└───────────────────────────────┘└─┘
typ    └────┘└───────────────────────────────┘└─┘
doc    └────┘                                 └─┘
txt    └────┘                                 └─┘
par    └────┘                                 └─┘
pid                                          └┘
st   ───────────────────────────────────────────┘
298  end
st   └─┘
299  
300  lemma convex_halfspace_lt {f : E → ℝ} (h : is_linear_map ℝ f) (r : ℝ) :
id                                            └───────────┘         
src                                            └───────────┘          
typ                                           └───────────┘         
301    convex {w | f w < r} :=
id     └────┘       
src    └────┘         
typ    └────┘       
doc    └────┘
302  (convex_Iio r).is_linear_preimage h
id    └────────┘  └────────────────┘  
src   └────────┘   └────────────────┘
typ   └────────┘  └────────────────┘  
303  
304  lemma convex_halfspace_le {f : E → ℝ} (h : is_linear_map ℝ f) (r : ℝ) :
id                                            └───────────┘         
src                                            └───────────┘          
typ                                           └───────────┘         
305    convex {w | f w ≤ r} :=
id     └────┘       
src    └────┘         
typ    └────┘       
doc    └────┘
306  (convex_Iic r).is_linear_preimage h
id    └────────┘  └────────────────┘  
src   └────────┘   └────────────────┘
typ   └────────┘  └────────────────┘  
307  
308  lemma convex_halfspace_gt {f : E → ℝ} (h : is_linear_map ℝ f) (r : ℝ) :
id                                            └───────────┘         
src                                            └───────────┘          
typ                                           └───────────┘         
309    convex {w | r < f w} :=
id     └────┘       
src    └────┘       
typ    └────┘       
doc    └────┘
310  (convex_Ioi r).is_linear_preimage h
id    └────────┘  └────────────────┘  
src   └────────┘   └────────────────┘
typ   └────────┘  └────────────────┘  
311  
312  lemma convex_halfspace_ge {f : E → ℝ} (h : is_linear_map ℝ f) (r : ℝ) :
id                                            └───────────┘         
src                                            └───────────┘          
typ                                           └───────────┘         
313    convex {w | r ≤ f w} :=
id     └────┘       
src    └────┘       
typ    └────┘       
doc    └────┘
314  (convex_Ici r).is_linear_preimage h
id    └────────┘  └────────────────┘  
src   └────────┘   └────────────────┘
typ   └────────┘  └────────────────┘  
315  
316  lemma convex_hyperplane {f : E → ℝ} (h : is_linear_map ℝ f) (r : ℝ) :
id                                          └───────────┘         
src                                          └───────────┘          
typ                                         └───────────┘         
317    convex {w | f w = r} :=
id     └────┘       
src    └────┘         
typ    └────┘       
doc    └────┘
318  begin
st   └─────
319    show convex (f ⁻¹' {p | p = r}),
id          └────┘   └─┘        
src    └───┘└────┘  └─┘└──┘  └┘
typ    └───┘└────┘ └─┘└──┘ └┘
doc    └───┘└────┘  └─┘ └──┘   └┘
txt    └───┘            └──┘   └┘
par    └───┘            └──┘   └┘
pid    └───┘            └──┘   └┘
st   ────────────────────────────────┘└─
320    rw set_of_eq_eq_singleton,
id        └────────────────────┘
src    └─┘└────────────────────┘
typ    └─┘└────────────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ──────────────────────────┘└─
321    exact (convex_singleton r).is_linear_preimage h
id            └──────────────┘                      
src    └────┘ └──────────────┘ └───────────────────┘ 
typ    └────┘ └──────────────┘└───────────────────┘
doc    └────┘                  └───────────────────┘ 
txt    └────┘                  └───────────────────┘ 
par    └────┘                  └───────────────────┘ 
pid                           └───────────────────┘ 
st   ─────────────────────────────────────────────────┘
322  end
st   └─┘
323  
324  lemma convex_halfspace_re_lt (r : ℝ) : convex {c : ℂ | c.re < r} :=
id                                         └────┘        └─┘  
src                                        └────┘         └─┘ 
typ                                        └────┘        └─┘  
doc                                         └────┘
325  convex_halfspace_lt (is_linear_map.mk complex.add_re complex.smul_re) _
id   └─────────────────┘  └──────────────┘ └────────────┘ └─────────────┘
src  └─────────────────┘  └──────────────┘ └────────────┘ └─────────────┘
typ  └─────────────────┘  └──────────────┘ └────────────┘ └─────────────┘
326  
327  lemma convex_halfspace_re_le (r : ℝ) : convex {c : ℂ | c.re ≤ r} :=
id                                         └────┘        └─┘  
src                                        └────┘         └─┘ 
typ                                        └────┘        └─┘  
doc                                         └────┘
328  convex_halfspace_le (is_linear_map.mk complex.add_re complex.smul_re) _
id   └─────────────────┘  └──────────────┘ └────────────┘ └─────────────┘
src  └─────────────────┘  └──────────────┘ └────────────┘ └─────────────┘
typ  └─────────────────┘  └──────────────┘ └────────────┘ └─────────────┘
329  
330  lemma convex_halfspace_re_gt (r : ℝ) : convex {c : ℂ | r < c.re } :=
id                                         └────┘          └─┘
src                                        └────┘            └─┘
typ                                        └────┘          └─┘
doc                                         └────┘
331  convex_halfspace_gt (is_linear_map.mk complex.add_re complex.smul_re) _
id   └─────────────────┘  └──────────────┘ └────────────┘ └─────────────┘
src  └─────────────────┘  └──────────────┘ └────────────┘ └─────────────┘
typ  └─────────────────┘  └──────────────┘ └────────────┘ └─────────────┘
332  
333  lemma convex_halfspace_re_lge (r : ℝ) : convex {c : ℂ | r ≤ c.re} :=
id                                          └────┘          └─┘
src                                         └────┘            └─┘
typ                                         └────┘          └─┘
doc                                          └────┘
334  convex_halfspace_ge (is_linear_map.mk complex.add_re complex.smul_re) _
id   └─────────────────┘  └──────────────┘ └────────────┘ └─────────────┘
src  └─────────────────┘  └──────────────┘ └────────────┘ └─────────────┘
typ  └─────────────────┘  └──────────────┘ └────────────┘ └─────────────┘
335  
336  lemma convex_halfspace_im_lt (r : ℝ) : convex {c : ℂ | c.im < r} :=
id                                         └────┘        └─┘  
src                                        └────┘         └─┘ 
typ                                        └────┘        └─┘  
doc                                         └────┘
337  convex_halfspace_lt (is_linear_map.mk complex.add_im complex.smul_im) _
id   └─────────────────┘  └──────────────┘ └────────────┘ └─────────────┘
src  └─────────────────┘  └──────────────┘ └────────────┘ └─────────────┘
typ  └─────────────────┘  └──────────────┘ └────────────┘ └─────────────┘
338  
339  lemma convex_halfspace_im_le (r : ℝ) : convex {c : ℂ | c.im ≤ r} :=
id                                         └────┘        └─┘  
src                                        └────┘         └─┘ 
typ                                        └────┘        └─┘  
doc                                         └────┘
340  convex_halfspace_le (is_linear_map.mk complex.add_im complex.smul_im) _
id   └─────────────────┘  └──────────────┘ └────────────┘ └─────────────┘
src  └─────────────────┘  └──────────────┘ └────────────┘ └─────────────┘
typ  └─────────────────┘  └──────────────┘ └────────────┘ └─────────────┘
341  
342  lemma convex_halfspace_im_gt (r : ℝ) : convex {c : ℂ | r < c.im } :=
id                                         └────┘          └─┘
src                                        └────┘            └─┘
typ                                        └────┘          └─┘
doc                                         └────┘
343  convex_halfspace_gt (is_linear_map.mk complex.add_im complex.smul_im) _
id   └─────────────────┘  └──────────────┘ └────────────┘ └─────────────┘
src  └─────────────────┘  └──────────────┘ └────────────┘ └─────────────┘
typ  └─────────────────┘  └──────────────┘ └────────────┘ └─────────────┘
344  
345  lemma convex_halfspace_im_lge (r : ℝ) : convex {c : ℂ | r ≤ c.im} :=
id                                          └────┘          └─┘
src                                         └────┘            └─┘
typ                                         └────┘          └─┘
doc                                          └────┘
346  convex_halfspace_ge (is_linear_map.mk complex.add_im complex.smul_im) _
id   └─────────────────┘  └──────────────┘ └────────────┘ └─────────────┘
src  └─────────────────┘  └──────────────┘ └────────────┘ └─────────────┘
typ  └─────────────────┘  └──────────────┘ └────────────┘ └─────────────┘
347  
348  section submodule
349  
350  open submodule
351  
352  lemma submodule.convex (K : submodule ℝ E) : convex (↑K : set E) :=
id                               └───────┘      └────┘     └─┘ 
src                              └───────┘       └────┘      └─┘
typ                              └───────┘      └────┘     └─┘ 
doc                              └───────┘        └────┘
353  by { repeat {intro}, refine add_mem _ (smul_mem _ _ _) (smul_mem _ _ _); assumption }
id                               └─────┘                     └──────┘
src       └──────┘└───┘  └─────┘└─────┘└─┘         └──────┘ └──────┘└─────┘  └─────────┘
typ       └──────┘└───┘  └─────┘└─────┘└─┘         └──────┘ └──────┘└─────┘  └─────────┘
doc       └──────┘└───┘  └─────┘       └─┘         └──────┘         └─────┘  └─────────┘
txt       └──────┘└───┘  └─────┘       └─┘         └──────┘         └─────┘  └─────────┘
par       └──────┘└───┘  └─────┘       └─┘         └──────┘         └─────┘  └─────────┘
pid             └──────┘               └─┘         └──────┘         └─────┘            
st     └──────────────┘└┘└──────────────────────────────────────────────────────────────┘└┘
354  
355  lemma subspace.convex (K : subspace ℝ E) : convex (↑K : set E) := K.convex
id                              └──────┘      └────┘     └─┘      └─────┘
src                             └──────┘       └────┘      └─┘        └─────┘
typ                             └──────┘      └────┘     └─┘      └─────┘
doc                             └──────┘        └────┘
356  
357  end submodule
358  
359  end sets
360  
361  section functions
362  
363  local notation `[`x `, ` y `]` := segment x y
id                                     └─────┘
src                                    └─────┘
typ                                    └─────┘
doc                                    └─────┘
364  
365  /-! ### Convex functions -/
366  
367  /-- Convexity of functions -/
368  def convex_on (s : set E) (f : E → ℝ) : Prop :=
id                      └─┘           
src                     └─┘             
typ                     └─┘           
369    convex s ∧
id     └────┘  
src    └────┘   
typ    └────┘  
doc    └────┘
370    ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 →
id                                                      
src                                                              
typ                                                     
371      f (a • x + b • y) ≤ a * f x + b * f y
id                          
src                                
typ                         
372  
373  variables {t : set E} {f g : E → ℝ}
id                  └─┘               
src                 └─┘               
typ                 └─┘               
374  
375  lemma convex_on_iff_div:
376    convex_on s f ↔ convex s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀  ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → 0 < a + b →
id     └───────┘    └────┘                                                       
src    └───────┘      └────┘                                                               
typ    └───────┘    └────┘                                                       
doc    └───────┘       └────┘
377      f ((a/(a+b)) • x + (b/(a+b)) • y) ≤ (a/(a+b)) * f x + (b/(a+b)) * f y :=
id                                          
src                                                        
typ                                         
378  and_congr iff.rfl
id   └───────┘ └─────┘
src  └───────┘ └─────┘
typ  └───────┘ └─────┘
379  ⟨begin
st    └─────
380    intros h x y hx hy a b ha hb hab,
src    └──────────────────────────────┘
typ    └──────────────────────────────┘
doc    └──────────────────────────────┘
txt    └──────────────────────────────┘
par    └──────────────────────────────┘
pid          └────────────────────────┘
st   ─────────────────────────────────┘└─
381    apply h hx hy (div_nonneg ha hab) (div_nonneg hb hab),
id            └┘ └┘             └┘       └────────┘ └┘ └─┘
src    └────┘                     └┘ └────────┘     
typ    └────┘└┘└┘           └┘   └┘ └────────┘└┘└─┘
doc    └────┘                     └┘                
txt    └────┘                     └┘                
par    └────┘                     └┘                
pid                              └┘                
st   ──────────────────────────────────────────────────────┘└─
382    rw [←add_div],
id          └─────┘
src    └───┘└─────┘
typ    └───┘└─────┘
doc    └───┘       
txt    └───┘       
par    └───┘       
pid      └─┘       
st   ─────────────┘└──
383    exact div_self (ne_of_gt hab)
id           └──────┘  └──────┘ └─┘
src    └────┘└──────┘ └──────┘   └┘
typ    └────┘└──────┘ └──────┘└─┘└┘
doc    └────┘                    └┘
txt    └────┘                    └┘
par    └────┘                    └┘
pid                             
st   ───────────────────────────────┘
384  end,
st   └─┘
385  begin
st   └─────
386    intros h x y hx hy a b ha hb hab,
src    └──────────────────────────────┘
typ    └──────────────────────────────┘
doc    └──────────────────────────────┘
txt    └──────────────────────────────┘
par    └──────────────────────────────┘
pid          └────────────────────────┘
st   ─────────────────────────────────┘└─
387    simpa [hab, zero_lt_one] using h hx hy ha hb,
id            └─┘  └─────────┘         └┘ └┘ └┘ └┘
src    └─────┘   └┘└─────────┘└──────┘       
typ    └─────┘└─┘└┘└─────────┘└──────┘└┘└┘└┘└┘
doc    └─────┘   └┘           └──────┘       
txt    └─────┘   └┘           └──────┘       
par    └─────┘   └┘           └──────┘       
pid            └┘           └────┘       
st   ─────────────────────────────────────────────┘└─
388  end⟩
st   ──┘
389  
390  /-- For a function on a convex set in a linear ordered space, in order to prove that it is convex
391  it suffices to verify the inequality `f (a • x + b • y) ≤ a * f x + b * f y` only for `x < y`
392  and positive `a`, `b`. The main use case is `E = ℝ` however one can apply it, e.g., to `ℝ^n` with
393  lexicographic order. -/
394  lemma linear_order.convex_on_of_lt [linear_order E] (hs : convex s)
id                                       └──────────┘         └────┘ 
src                                      └──────────┘          └────┘
typ                                      └──────────┘         └────┘ 
doc                                                            └────┘
395    (hf : ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → x < y → ∀ ⦃a b : ℝ⦄, 0 < a → 0 < b → a + b = 1 →
id                                                                 
src                                                                           
typ                                                                
396      f (a • x + b • y) ≤ a * f x + b * f y) : convex_on s f :=
id                              └───────┘  
src                                        └───────┘
typ                             └───────┘  
doc                                               └───────┘
397  begin
st   └─────
398    use hs,
id         └┘
src    └──┘
typ    └──┘└┘
doc    └──┘
txt    └──┘
par    └──┘
pid       
st   ───────┘└─
399    intros x y hx hy a b ha hb hab,
src    └────────────────────────────┘
typ    └────────────────────────────┘
doc    └────────────────────────────┘
txt    └────────────────────────────┘
par    └────────────────────────────┘
pid          └──────────────────────┘
st   ───────────────────────────────┘└─
400    wlog hxy : x<=y using [x y a b, y x b a],
id                └┘
src    └─────────┘ └┘ └───────────────────────┘
typ    └─────────┘└┘└───────────────────────┘
doc    └─────────┘    └───────────────────────┘
txt    └─────────┘    └───────────────────────┘
par    └─────────┘    └───────────────────────┘
pid        └──┘└─┘    └──────────────────────┘
st   ─────────────────────────────────────────┘└─
401    { exact le_total _ _ },
id             └──────┘
src      └────┘└──────┘└───┘
typ      └────┘└──────┘└───┘
doc      └────┘        └───┘
txt      └────┘        └───┘
par      └────┘        └───┘
pid                   └──┘
st   ───┘└─────────────────┘└┘
402    { cases eq_or_lt_of_le hxy with hxy hxy,
id             └────────────┘ └─┘
src      └────┘└────────────┘   └───────────┘
typ      └────┘└────────────┘└─┘└───────────┘
doc      └────┘                 └───────────┘
txt      └────┘                 └───────────┘
par      └────┘                 └───────────┘
pid                            └───────────┘
st   ────────────────────────────────────────┘
403        by { subst y, rw [← add_smul, ← add_mul, hab, one_smul, one_mul] },
id                            └──────┘    └─────┘  └─┘  └──────┘  └─────┘
src             └────┘   └────┘└──────┘└──┘└─────┘└┘   └┘└──────┘└┘└─────┘└┘
typ             └────┘  └────┘└──────┘└──┘└─────┘└┘└─┘└┘└──────┘└┘└─────┘└┘
doc             └────┘   └────┘        └──┘       └┘   └┘        └┘       └┘
txt             └────┘   └────┘        └──┘       └┘   └┘        └┘       └┘
par             └────┘   └────┘        └──┘       └┘   └┘        └┘       └┘
pid                       └──┘        └──┘       └┘   └┘        └┘       
st            └──────┘└──────────────┘└─────────┘└───┘└────────┘└───────┘└┘
404      cases eq_or_lt_of_le ha with ha ha,
id             └────────────┘ └┘
src      └────┘└────────────┘  └─────────┘
typ      └────┘└────────────┘└┘└─────────┘
doc      └────┘                └─────────┘
txt      └────┘                └─────────┘
par      └────┘                └─────────┘
pid                           └─────────┘
st   ─────────────────────────────────────┘
405        by { subst a, rw [zero_add] at hab, subst b, simp },
id                          └──────┘                
src             └────┘   └──┘└──────┘└──────┘  └────┘   └───┘
typ             └────┘  └──┘└──────┘└──────┘  └────┘  └───┘
doc             └────┘   └──┘        └──────┘  └────┘   └───┘
txt             └────┘   └──┘        └──────┘  └────┘   └───┘
par             └────┘   └──┘        └──────┘  └────┘   └───┘
pid                       └┘        └─────┘              
st            └──────┘└────────────┘└─────┘└───────┘└─────┘└┘
406      cases eq_or_lt_of_le hb with hb hb,
id             └────────────┘ └┘
src      └────┘└────────────┘  └─────────┘
typ      └────┘└────────────┘└┘└─────────┘
doc      └────┘                └─────────┘
txt      └────┘                └─────────┘
par      └────┘                └─────────┘
pid                           └─────────┘
st   ─────────────────────────────────────┘
407        by { subst b, rw [add_zero] at hab, subst a, simp },
id                          └──────┘                
src             └────┘   └──┘└──────┘└──────┘  └────┘   └───┘
typ             └────┘  └──┘└──────┘└──────┘  └────┘  └───┘
doc             └────┘   └──┘        └──────┘  └────┘   └───┘
txt             └────┘   └──┘        └──────┘  └────┘   └───┘
par             └────┘   └──┘        └──────┘  └────┘   └───┘
pid                       └┘        └─────┘              
st            └──────┘└────────────┘└─────┘└───────┘└─────┘└┘
408      exact hf hx hy hxy ha hb hab }
id             └┘ └┘ └┘ └─┘ └┘ └┘ └─┘
src      └────┘                
typ      └────┘└┘└┘└┘└─┘└┘└┘└─┘
doc      └────┘                
txt      └────┘                
par      └────┘                
pid                           
st   ────────────────────────────────┘└─
409  end
st   ──┘
410  
411  /-- For a function `f` defined on a convex subset `D` of `ℝ`, if for any three points `x<y<z`
412  the slope of the secant line of `f` on `[x, y]` is less than or equal to the slope
413  of the secant line of `f` on `[x, z]`, then `f` is convex on `D`. This way of proving convexity
414  of a function is used in the proof of convexity of a function with a monotone derivative. -/
415  lemma convex_on_real_of_slope_mono_adjacent {s : set ℝ} (hs : convex s) {f : ℝ → ℝ}
id                                                    └─┘         └────┘           
src                                                   └─┘         └────┘            
typ                                                   └─┘         └────┘           
doc                                                                └────┘
416    (hf : ∀ {x y z : ℝ}, x ∈ s → z ∈ s → x < y → y < z →
id                                          
src                                               
typ                                         
417      (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)) :
id                                
src                                         
typ                               
418    convex_on s f :=
id     └───────┘  
src    └───────┘
typ    └───────┘  
doc    └───────┘
419  linear_order.convex_on_of_lt hs
id   └──────────────────────────┘ └┘
src  └──────────────────────────┘
typ  └──────────────────────────┘ └┘
doc  └──────────────────────────┘
420  begin
st   └─────
421    assume x z hx hz hxz a b ha hb hab,
src    └────────────────────────────────┘
typ    └────────────────────────────────┘
doc    └────────────────────────────────┘
txt    └────────────────────────────────┘
par    └────────────────────────────────┘
pid    └────────────────────────────────┘
st   ───────────────────────────────────┘└─
422    let y := a * x + b * z,
id                     
src    └───────┘    
typ    └───────┘ 
doc    └───────┘      
txt    └───────┘      
par    └───────┘      
pid    └───┘└─┘      
st   ───────────────────────┘└─
423    have hxy : x < y,
id                  
src    └─────────┘ 
typ    └─────────┘
doc    └─────────┘  
txt    └─────────┘  
par    └─────────┘  
pid    └──────┘└─┘  
st   ─────────────────┘└─
424    { rw [← one_mul x, ← hab, add_mul],
id             └─────┘     └─┘  └─────┘
src      └────┘└─────┘ └──┘   └┘└─────┘
typ      └────┘└─────┘└──┘└─┘└┘└─────┘
doc      └────┘        └──┘   └┘       
txt      └────┘        └──┘   └┘       
par      └────┘        └──┘   └┘       
pid        └──┘        └──┘   └┘       
st   ───┘└─────────────┘└─────┘└───────┘└──
425      exact add_lt_add_left ((mul_lt_mul_left hb).2 hxz) _ },
id             └─────────────┘   └─────────────┘ └┘    └─┘
src      └────┘└─────────────┘  └─────────────┘  └──┘   └──┘
typ      └────┘└─────────────┘  └─────────────┘└┘└──┘└─┘└──┘
doc      └────┘                                  └──┘   └──┘
txt      └────┘                                  └──┘   └──┘
par      └────┘                                  └──┘   └──┘
pid                                             └──┘   └─┘
st   ────────────────────────────────────────────────────────┘└┘
426    have hyz : y < z,
id                   
src    └─────────┘  
typ    └─────────┘ 
doc    └─────────┘  
txt    └─────────┘  
par    └─────────┘  
pid    └──────┘└─┘  
st   ─────────────────┘└─
427    { rw [← one_mul z, ← hab, add_mul],
id             └─────┘     └─┘  └─────┘
src      └────┘└─────┘ └──┘   └┘└─────┘
typ      └────┘└─────┘└──┘└─┘└┘└─────┘
doc      └────┘        └──┘   └┘       
txt      └────┘        └──┘   └┘       
par      └────┘        └──┘   └┘       
pid        └──┘        └──┘   └┘       
st   ───┘└─────────────┘└─────┘└───────┘└──
428      exact add_lt_add_right ((mul_lt_mul_left ha).2 hxz) _ },
id             └──────────────┘   └─────────────┘ └┘    └─┘
src      └────┘└──────────────┘  └─────────────┘  └──┘   └──┘
typ      └────┘└──────────────┘  └─────────────┘└┘└──┘└─┘└──┘
doc      └────┘                                   └──┘   └──┘
txt      └────┘                                   └──┘   └──┘
par      └────┘                                   └──┘   └──┘
pid                                              └──┘   └─┘
st   ─────────────────────────────────────────────────────────┘└┘
429    have : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x),
id                                                  
src    └─────┘     └┘     └┘      └┘     
typ    └─────┘     └┘     └┘    └┘   
doc    └─────┘      └┘     └┘       └┘     
txt    └─────┘      └┘     └┘       └┘     
par    └─────┘      └┘     └┘       └┘     
pid    └───┘└┘      └┘     └┘       └┘     
st   ─────────────────────────────────────────────────────┘└─
430      from (div_le_div_iff (sub_pos.2 hxy) (sub_pos.2 hyz)).1 (hf hx hz hxy hyz),
id             └────────────┘                  └─────┘            └┘ └┘ └┘ └─┘ └─┘
src      └───┘ └────────────┘        └─┘   └┘ └─────┘└─┘   └───┘             
typ      └───┘ └────────────┘        └─┘   └┘ └─────┘└─┘   └───┘ └┘└┘└┘└─┘└─┘
doc      └───┘                       └─┘   └┘        └─┘   └───┘             
txt      └───┘                       └─┘   └┘        └─┘   └───┘             
par      └───┘                       └─┘   └┘        └─┘   └───┘             
pid      └───┘                       └─┘   └┘        └─┘   └───┘             
st   ─────────────────────────────────────────────────────────────────────────────┘└─
431    have A : z - y + (y - x) = z - x, by abel,
id                                 
src    └───────┘        └┘        └──┘
typ    └───────┘       └┘      └──┘
doc    └───────┘        └┘         └──┘
txt    └───────┘        └┘         └──┘
par    └───────┘        └┘         └──┘
pid    └────┘└─┘        └┘   
st   ─────────────────────────────────┘         └─
432    have B : 0 < z - x, from sub_pos.2 (lt_trans hxy hyz),
id                            └─────┘    └──────┘ └─┘ └─┘
src    └─────────┘      └───┘└─────┘└─┘ └──────┘      
typ    └─────────┘    └───┘└─────┘└─┘ └──────┘└─┘└─┘
doc    └─────────┘      └───┘       └─┘               
txt    └─────────┘      └───┘       └─┘               
par    └─────────┘      └───┘       └─┘               
pid    └────┘└───┘      └───┘       └─┘               
st   ───────────────────┘└─────────────────────────────────┘└─
433    rw [sub_mul, sub_mul, sub_le_iff_le_add', ← add_sub_assoc, le_sub_iff_add_le, ← mul_add, A,
id         └─────┘  └─────┘  └────────────────┘    └───────────┘  └───────────────┘    └─────┘  
src    └──┘└─────┘└┘└─────┘└┘└────────────────┘└──┘└───────────┘└┘└───────────────┘└──┘└─────┘└┘ └─
typ    └──┘└─────┘└┘└─────┘└┘└────────────────┘└──┘└───────────┘└┘└───────────────┘└──┘└─────┘└┘└─
doc    └──┘       └┘       └┘                  └──┘             └┘                 └──┘       └┘ └─
txt    └──┘       └┘       └┘                  └──┘             └┘                 └──┘       └┘ └─
par    └──┘       └┘       └┘                  └──┘             └┘                 └──┘       └┘ └─
pid      └┘       └┘       └┘                  └──┘             └┘                 └──┘       └┘ └─
st   ────────────┘└───────┘└──────────────────┘└───────────────┘└─────────────────┘└─────────┘└─┘└─
434      ← le_div_iff B, add_div, mul_div_assoc, mul_div_assoc,
id         └────────┘   └─────┘  └───────────┘  └───────────┘
src  ─────┘└────────┘ └┘└─────┘└┘└───────────┘└┘└───────────┘└─
typ  ─────┘└────────┘└┘└─────┘└┘└───────────┘└┘└───────────┘└─
doc  ─────┘           └┘       └┘             └┘             └─
txt  ─────┘           └┘       └┘             └┘             └─
par  ─────┘           └┘       └┘             └┘             └─
pid  ─────┘           └┘       └┘             └┘             └─
st   ─────────────────┘└───────┘└─────────────┘└─────────────┘└─
435      mul_comm (f x), mul_comm (f z)] at this,
id       └──────┘      └──────┘   
src  ───┘└──────┘   └─┘└──────┘   └────────┘
typ  ───┘└──────┘ └─┘└──────┘ └────────┘
doc  ───┘           └─┘           └────────┘
txt  ───┘           └─┘           └────────┘
par  ───┘           └─┘           └────────┘
pid  ───┘           └─┘           └┘└──────┘
st   ─────────────────┘└──────────────┘└──────┘└─
436    rw [eq_comm, ← sub_eq_iff_eq_add] at hab; subst a,
id         └─────┘    └───────────────┘                
src    └──┘└─────┘└──┘└───────────────┘└──────┘  └────┘
typ    └──┘└─────┘└──┘└───────────────┘└──────┘  └────┘
doc    └──┘       └──┘                 └──────┘  └────┘
txt    └──┘       └──┘                 └──────┘  └────┘
par    └──┘       └──┘                 └──────┘  └────┘
pid      └┘       └──┘                 └─────┘       
st   ────────────┘└───────────────────┘└──────────────┘└─
437    convert this; symmetry; simp only [div_eq_iff (ne_of_gt B), y]; ring
id             └──┘                       └────────┘  └──────┘    
src    └──────┘      └──────┘  └─────────┘└────────┘ └──────┘ └─┘   └───┘
typ    └──────┘└──┘  └──────┘  └─────────┘└────────┘ └──────┘└─┘  └───┘
doc    └──────┘      └──────┘  └─────────┘                    └─┘   └───┘
txt    └──────┘      └──────┘  └─────────┘                    └─┘   └───┘
par    └──────┘      └──────┘  └─────────┘                    └─┘   └───┘
pid                               └──┘└┘                    └─┘       
st   ──────────────────────────────────────────────────────────────────────┘
438  end
st   └─┘
439  
440  lemma convex_on.subset (h_convex_on : convex_on t f) (h_subset : s ⊆ t) (h_convex : convex s) :
id                                         └───────┘                                └────┘ 
src                                        └───────┘                                    └────┘
typ                                        └───────┘                                └────┘ 
doc                                        └───────┘                                     └────┘
441    convex_on s f :=
id     └───────┘  
src    └───────┘
typ    └───────┘  
doc    └───────┘
442  begin
st   └─────
443    apply and.intro h_convex,
id           └───────┘ └──────┘
src    └────┘└───────┘
typ    └────┘└───────┘└──────┘
doc    └────┘         
txt    └────┘         
par    └────┘         
pid                  
st   ─────────────────────────┘└─
444    intros x y hx hy,
src    └──────────────┘
typ    └──────────────┘
doc    └──────────────┘
txt    └──────────────┘
par    └──────────────┘
pid          └────────┘
st   ─────────────────┘└─
445    exact h_convex_on.2 (h_subset hx) (h_subset hy),
id           └─────────┘             └┘   └──────┘ └┘
src    └────┘           └─┘           └┘           
typ    └────┘└─────────┘└─┘         └┘└┘ └──────┘└┘
doc    └────┘           └─┘           └┘           
txt    └────┘           └─┘           └┘           
par    └────┘           └─┘           └┘           
pid                    └─┘           └┘           
st   ────────────────────────────────────────────────┘└─
446  end
st   ──┘
447  
448  lemma convex_on.add (hf : convex_on s f) (hg : convex_on s g) : convex_on s (λx, f x + g x) :=
id                             └───────┘          └───────┘      └───────┘          
src                            └───────┘            └───────┘        └───────┘            
typ                            └───────┘          └───────┘      └───────┘          
doc                            └───────┘            └───────┘        └───────┘
449  begin
st   └─────
450    apply and.intro hf.1,
id           └───────┘ └┘
src    └────┘└───────┘  └┘
typ    └────┘└───────┘└┘└┘
doc    └────┘           └┘
txt    └────┘           └┘
par    └────┘           └┘
pid                    └┘
st   ─────────────────────┘└─
451    intros x y hx hy a b ha hb hab,
src    └────────────────────────────┘
typ    └────────────────────────────┘
doc    └────────────────────────────┘
txt    └────────────────────────────┘
par    └────────────────────────────┘
pid          └──────────────────────┘
st   ───────────────────────────────┘└─
452    calc
id     └──┘
src    └──┘
typ    └──┘
doc    └──┘
st   ───────
453      f (a • x + b • y) + g (a • x + b • y) ≤ (a * f x + b * f y) + (a * g x + b * g y)
id                                                                               
src                       
typ                                                                              
st   ──────────────────────────────────────────────────────────────────────────────────────
454        : add_le_add (hf.2 hx hy ha hb hab) (hg.2 hx hy ha hb hab)
id           └────────┘  └┘                    └┘  └┘ └┘ └┘ └┘ └─┘
src          └────────┘                          
typ          └────────┘  └┘                    └┘  └┘ └┘ └┘ └┘ └─┘
st   ─────────────────────────────────────────────────────────────────
455      ... = a * f x + a * g x + b * f y + b * g y : by linarith
id               
src                                                      └────────
typ                                                      └────────
doc                                                       └────────
txt                                                       └────────
par                                                       └────────
pid                                                               
st   ───────────────────────────────────────────────────┘└─────────
456      ... = a * (f x + g x) + b * (f y + g y) : by simp [mul_add]
id                                                          └─────┘
src  ───┘                                             └────┘└─────┘└┘
typ  ───┘                                             └────┘└─────┘└┘
doc  ───┘                                             └────┘       └┘
txt  ───┘                                             └────┘       └┘
par  ───┘                                             └────┘       └┘
pid  ───┘                                                        
st   ───┘└──────────────────────────────────────────┘└──────────────┘
457  end
st   └─┘
458  
459  lemma convex_on.smul {c : ℝ} (hc : 0 ≤ c) (hf : convex_on s f) : convex_on s (λx, c * f x) :=
id                                                └───────┘      └───────┘         
src                                                └───────┘        └───────┘          
typ                                               └───────┘      └───────┘         
doc                                                  └───────┘        └───────┘
460  begin
st   └─────
461    apply and.intro hf.1,
id           └───────┘ └┘
src    └────┘└───────┘  └┘
typ    └────┘└───────┘└┘└┘
doc    └────┘           └┘
txt    └────┘           └┘
par    └────┘           └┘
pid                    └┘
st   ─────────────────────┘└─
462    intros x y hx hy a b ha hb hab,
src    └────────────────────────────┘
typ    └────────────────────────────┘
doc    └────────────────────────────┘
txt    └────────────────────────────┘
par    └────────────────────────────┘
pid          └──────────────────────┘
st   ───────────────────────────────┘└─
463    calc
id     └──┘
src    └──┘
typ    └──┘
doc    └──┘
st   ───────
464      c * f (a • x + b • y) ≤ c * (a * f x + b * f y)
id                  
src                 
typ                 
st   ────────────────────────────────────────────────────
465        : mul_le_mul_of_nonneg_left (hf.2 hx hy ha hb hab) hc
id           └───────────────────────┘  └┘  └┘ └┘ └┘ └┘ └─┘  └┘
src          └───────────────────────┘    
typ          └───────────────────────┘  └┘  └┘ └┘ └┘ └┘ └─┘  └┘
st   ────────────────────────────────────────────────────────────
466      ... = a * (c * f x) + b * (c * f y) : by rw mul_add; ac_refl
id                                             └─────┘
src                                               └─┘└─────┘  └──────┘
typ                                         └─┘└─────┘  └──────┘
doc                                               └─┘         └──────┘
txt                                               └─┘         └──────┘
par                                               └─┘         └──────┘
pid                                                                 
st   ───────────────────────────────────────────┘└───────────────────┘
467  end
st   └─┘
468  
469  lemma convex_on.le_on_segment' {x y : E} {a b : ℝ}
id                                                  
src                                                  
typ                                                 
470    (hf : convex_on s f) (hx : x ∈ s) (hy : y ∈ s) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :
id           └───────┘                                                        
src          └───────┘                                                                  
typ          └───────┘                                                        
doc          └───────┘
471    f (a • x + b • y) ≤ max (f x) (f y) :=
id                └─┘       
src                    └─┘
typ               └─┘       
472  calc
473    f (a • x + b • y) ≤ a * f x + b * f y : hf.2 hx hy ha hb hab
id                            └┘  └┘ └┘ └┘ └┘ └─┘
src                                        
typ                           └┘  └┘ └┘ └┘ └┘ └─┘
474    ... ≤ a * max (f x) (f y) + b * max (f x) (f y) :
id             └─┘            └─┘       
src             └─┘                 └─┘
typ            └─┘            └─┘       
475      add_le_add (mul_le_mul_of_nonneg_left (le_max_left _ _) ha) (mul_le_mul_of_nonneg_left (le_max_right _ _) hb)
id       └────────┘  └───────────────────────┘  └─────────┘      └┘   └───────────────────────┘  └──────────┘      └┘
src      └────────┘  └───────────────────────┘  └─────────┘           └───────────────────────┘  └──────────┘
typ      └────────┘  └───────────────────────┘  └─────────┘      └┘   └───────────────────────┘  └──────────┘      └┘
476    ... ≤ max (f x) (f y) : by rw [←add_mul, hab, one_mul]
id           └─┘                   └─────┘  └─┘  └─────┘
src          └─┘                  └───┘└─────┘└┘   └┘└─────┘└─
typ          └─┘              └───┘└─────┘└┘└─┘└┘└─────┘└─
doc                               └───┘       └┘   └┘       └─
txt                               └───┘       └┘   └┘       └─
par                               └───┘       └┘   └┘       └─
pid                                 └─┘       └┘   └┘       
st                               └───────────┘└───┘└───────┘
477  
src  
typ  
doc  
txt  
par  
pid  
st   
478  lemma convex_on.le_on_segment (hf : convex_on s f) {x y z : E}
id                                       └───────┘             
src                                      └───────┘
typ                                      └───────┘             
doc                                      └───────┘
479    (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ [x, y]) :
id                                  
src                                        
typ                                 
doc                                           
480    f z ≤ max (f x) (f y) :=
id        └─┘       
src         └─┘
typ       └─┘       
481  let ⟨a, b, ha, hb, hab, hz⟩ := hz in hz ▸ hf.le_on_segment' hx hy ha hb hab
id   └─┘        └┘  └┘  └─┘  └┘     └┘        └┘└─────────────┘ └┘ └┘
src                                             └─────────────┘
typ  └─┘        └┘  └┘  └─┘  └┘     └┘        └┘└─────────────┘ └┘ └┘
482  
483  lemma convex_on.convex_le (hf : convex_on s f) (r : ℝ) : convex {x ∈ s | f x ≤ r} :=
id                                   └───────┘             └────┘           
src                                  └───────┘               └────┘             
typ                                  └───────┘             └────┘           
doc                                  └───────┘                └────┘
484  convex_iff_segment_subset.2 $ λ x y hx hy z hz,
id   └───────────────────────┘        └┘ └┘  └┘
src  └───────────────────────┘
typ  └───────────────────────┘        └┘ └┘  └┘
485    ⟨hf.1.segment_subset hx.1 hy.1 hz,
id      └┘ └────────────┘  └┘  └┘  └┘
src        └────────────┘        
typ     └┘ └────────────┘  └┘  └┘  └┘
486      le_trans (hf.le_on_segment hx.1 hy.1 hz) $ max_le hx.2 hy.2⟩
id       └──────┘  └┘└────────────┘ └┘  └┘  └┘    └────┘ └┘  └┘
src      └──────┘    └────────────┘               └────┘       
typ      └──────┘  └┘└────────────┘ └┘  └┘  └┘    └────┘ └┘  └┘
487  
488  lemma convex_on.convex_lt (hf : convex_on s f) (r : ℝ) : convex {x ∈ s | f x < r} :=
id                                   └───────┘             └────┘           
src                                  └───────┘               └────┘             
typ                                  └───────┘             └────┘           
doc                                  └───────┘                └────┘
489  convex_iff_segment_subset.2 $ λ x y hx hy z hz,
id   └───────────────────────┘        └┘ └┘  └┘
src  └───────────────────────┘
typ  └───────────────────────┘        └┘ └┘  └┘
490    ⟨hf.1.segment_subset hx.1 hy.1 hz,
id      └┘ └────────────┘  └┘  └┘  └┘
src        └────────────┘        
typ     └┘ └────────────┘  └┘  └┘  └┘
491      lt_of_le_of_lt (hf.le_on_segment hx.1 hy.1 hz) $ max_lt hx.2 hy.2⟩
id       └────────────┘  └┘└────────────┘ └┘  └┘  └┘    └────┘ └┘  └┘
src      └────────────┘    └────────────┘               └────┘       
typ      └────────────┘  └┘└────────────┘ └┘  └┘  └┘    └────┘ └┘  └┘
492  
493  lemma convex_on.convex_epigraph (hf : convex_on s f) :
id                                         └───────┘  
src                                        └───────┘
typ                                        └───────┘  
doc                                        └───────┘
494    convex {p : E × ℝ | p.1 ∈ s ∧ f p.1 ≤ p.2} :=
id     └────┘                   
src    └────┘                         
typ    └────┘                   
doc    └────┘
495  begin
st   └─────
496    rintros ⟨x, r⟩ ⟨y, t⟩ ⟨hx, hr⟩ ⟨hy, ht⟩ a b ha hb hab,
src    └───────────────────────────────────────────────────┘
typ    └───────────────────────────────────────────────────┘
doc    └───────────────────────────────────────────────────┘
txt    └───────────────────────────────────────────────────┘
par    └───────────────────────────────────────────────────┘
pid           └────────────────────────────────────────────┘
st   ──────────────────────────────────────────────────────┘└─
497    refine ⟨hf.1 hx hy ha hb hab, _⟩,
id             └┘   └┘ └┘ └┘ └┘ └─┘
src    └─────┘   └─┘           └──┘
typ    └─────┘ └┘└─┘└┘└┘└┘└┘└─┘└──┘
doc    └─────┘   └─┘           └──┘
txt    └─────┘   └─┘           └──┘
par    └─────┘   └─┘           └──┘
pid             └─┘           └──┘
st   ─────────────────────────────────┘└─
498    calc f (a • x + b • y) ≤ a * f x + b * f y : hf.2 hx hy ha hb hab
id     └──┘                                   └┘  └┘ └┘       └─┘
src    └──┘                                        
typ    └──┘                                   └┘  └┘ └┘       └─┘
doc    └──┘
st   ────────────────────────────────────────────────────────────────────
499    ... ≤ a * r + b * t : add_le_add (mul_le_mul_of_nonneg_left hr ha)
id                       └────────┘                            └┘ └┘
src                          └────────┘
typ                      └────────┘                            └┘ └┘
st   ─────────────────────────────────────────────────────────────────────
500      (mul_le_mul_of_nonneg_left ht hb)
id        └───────────────────────┘ └┘ └┘
src       └───────────────────────┘
typ       └───────────────────────┘ └┘ └┘
st   ────────────────────────────────────┘
501  end
st   ──┘
502  
503  lemma convex_on_iff_convex_epigraph : convex_on s f ↔ convex {p : E × ℝ | p.1 ∈ s ∧ f p.1 ≤ p.2} :=
id                                         └───────┘    └────┘                   
src                                        └───────┘      └────┘                         
typ                                        └───────┘    └────┘                   
doc                                        └───────┘       └────┘
504  begin
st   └─────
505    refine ⟨convex_on.convex_epigraph, λ h, ⟨_, _⟩⟩,
id             └───────────────────────┘
src    └─────┘ └───────────────────────┘└┘ └──┘ └────┘
typ    └─────┘ └───────────────────────┘└┘ └──┘ └────┘
doc    └─────┘                          └┘ └──┘ └────┘
txt    └─────┘                          └┘ └──┘ └────┘
par    └─────┘                          └┘ └──┘ └────┘
pid                                    └┘ └──┘ └────┘
st   ────────────────────────────────────────────────┘└─
506    { assume x y hx hy a b ha hb hab,
src      └────────────────────────────┘
typ      └────────────────────────────┘
doc      └────────────────────────────┘
txt      └────────────────────────────┘
par      └────────────────────────────┘
pid      └────────────────────────────┘
st   ───┘└────────────────────────────┘└─
507      exact (@h (x, f x) (y, f y) ⟨hx, le_refl _⟩ ⟨hy, le_refl _⟩ a b ha hb hab).1 },
id                               └┘              └┘  └─────┘      └┘ └┘ └─┘
src      └────┘    └┘  └┘  └┘  └┘   └┘       └──┘   └┘└─────┘└──┘         └──┘
typ      └────┘   └┘ └┘  └┘└┘ └┘└┘       └──┘ └┘└┘└─────┘└──┘└┘└┘└─┘└──┘
doc      └────┘     └┘  └┘  └┘  └┘   └┘       └──┘   └┘       └──┘         └──┘
txt      └────┘     └┘  └┘  └┘  └┘   └┘       └──┘   └┘       └──┘         └──┘
par      └────┘     └┘  └┘  └┘  └┘   └┘       └──┘   └┘       └──┘         └──┘
pid                └┘  └┘  └┘  └┘   └┘       └──┘   └┘       └──┘         └─┘
st   ────────────────────────────────────────────────────────────────────────────────┘└┘
508    { assume x y hx hy a b ha hb hab,
src      └────────────────────────────┘
typ      └────────────────────────────┘
doc      └────────────────────────────┘
txt      └────────────────────────────┘
par      └────────────────────────────┘
pid      └────────────────────────────┘
st   ─────────────────────────────────┘└─
509      exact (@h (x, f x) (y, f y) ⟨hx, le_refl _⟩ ⟨hy, le_refl _⟩ a b ha hb hab).2 }
id                                └┘              └┘  └─────┘      └┘ └┘ └─┘
src      └────┘     └┘  └┘  └┘  └┘   └┘       └──┘   └┘└─────┘└──┘         └──┘
typ      └────┘    └┘ └┘  └┘└┘ └┘└┘       └──┘ └┘└┘└─────┘└──┘└┘└┘└─┘└──┘
doc      └────┘     └┘  └┘  └┘  └┘   └┘       └──┘   └┘       └──┘         └──┘
txt      └────┘     └┘  └┘  └┘  └┘   └┘       └──┘   └┘       └──┘         └──┘
par      └────┘     └┘  └┘  └┘  └┘   └┘       └──┘   └┘       └──┘         └──┘
pid                └┘  └┘  └┘  └┘   └┘       └──┘   └┘       └──┘         └─┘
st   ────────────────────────────────────────────────────────────────────────────────┘└─
510  end
st   ──┘
511  
512  end functions
513  
514  section center_mass
515  
516  /-- Center mass of a finite collection of points with prescribed weights.
517  Note that we require neither `0 ≤ w i` nor `∑ w = 1`. -/
518  noncomputable def finset.center_mass (t : finset ι) (w : ι → ℝ) (z : ι → E) : E :=
id                                             └────┘                         
src                                            └────┘             
typ                                            └────┘                         
doc                                            └────┘
519  (t.sum w)⁻¹ • (t.sum (λ i, w i • z i))
id    └──┘  └┘   └──┘          
src    └──┘   └┘    └──┘           
typ   └──┘  └┘   └──┘          
520  
521  variables (i j : ι) (c : ℝ) (t : finset ι) (w : ι → ℝ) (z : ι → E)
id                                   └────┘             
src                                  └────┘             
typ                                  └────┘             
doc                                   └────┘
522  
523  open finset (hiding singleton)
524  
525  lemma finset.center_mass_empty : (∅ : finset ι).center_mass w z = 0 :=
id                                        └────┘  └─────────┘    
src                                       └────┘   └─────────┘      
typ                                       └────┘  └─────────┘    
doc                                        └────┘   └─────────┘
526  by simp only [center_mass, sum_empty, smul_zero]
id                 └─────────┘  └───────┘  └───────┘
src     └─────────┘└─────────┘└┘└───────┘└┘└───────┘└─
typ     └─────────┘└─────────┘└┘└───────┘└┘└───────┘└─
doc     └─────────┘└─────────┘└┘         └┘         └─
txt     └─────────┘           └┘         └┘         └─
par     └─────────┘           └┘         └┘         └─
pid         └──┘└┘           └┘         └┘         
st     └──────────────────────────────────────────────
527  
src  
typ  
doc  
txt  
par  
pid  
st   
528  lemma finset.center_mass_pair (hne : i ≠ j) :
id                                          
src                                         
typ                                         
529    ({i, j} : finset ι).center_mass w z = (w i / (w i + w j)) • z i + (w j / (w i + w j)) • z j :=
id           └────┘  └─────────┘                                   
src            └────┘   └─────────┘                                                 
typ          └────┘  └─────────┘                                   
doc              └────┘   └─────────┘
530  by simp only [center_mass, sum_pair hne, smul_add, (mul_smul _ _ _).symm, div_eq_inv_mul]
id                 └─────────┘  └──────┘ └─┘  └──────┘   └──────┘              └────────────┘
src     └─────────┘└─────────┘└┘└──────┘   └┘└──────┘└┘ └──────┘└────────────┘└────────────┘└─
typ     └─────────┘└─────────┘└┘└──────┘└─┘└┘└──────┘└┘ └──────┘└────────────┘└────────────┘└─
doc     └─────────┘└─────────┘└┘           └┘        └┘         └────────────┘              └─
txt     └─────────┘           └┘           └┘        └┘         └────────────┘              └─
par     └─────────┘           └┘           └┘        └┘         └────────────┘              └─
pid         └──┘└┘           └┘           └┘        └┘         └────────────┘              
st     └───────────────────────────────────────────────────────────────────────────────────────
531  
src  
typ  
doc  
txt  
par  
pid  
st   
532  variable {w}
533  
534  lemma finset.center_mass_insert (ha : i ∉ t) (hw : t.sum w ≠ 0) :
id                                                   └──┘  
src                                                     └──┘   
typ                                                  └──┘  
535    (insert i t).center_mass w z = (w i / (w i + t.sum w)) • z i +
id      └────┘   └─────────┘             └──┘       
src     └────┘     └─────────┘                    └──┘          
typ     └────┘   └─────────┘             └──┘       
doc                └─────────┘
536      (t.sum w / (w i + t.sum w)) • t.center_mass w z :=
id        └──┘       └──┘     └──────────┘  
src        └──┘           └──┘       └──────────┘
typ       └──┘       └──┘     └──────────┘  
doc                                     └──────────┘
537  begin
st   └─────
538    simp only [center_mass, sum_insert ha, smul_add, (mul_smul _ _ _).symm],
id                └─────────┘  └────────┘ └┘  └──────┘   └──────┘
src    └─────────┘└─────────┘└┘└────────┘  └┘└──────┘└┘ └──────┘└───────────┘
typ    └─────────┘└─────────┘└┘└────────┘└┘└┘└──────┘└┘ └──────┘└───────────┘
doc    └─────────┘└─────────┘└┘            └┘        └┘         └───────────┘
txt    └─────────┘           └┘            └┘        └┘         └───────────┘
par    └─────────┘           └┘            └┘        └┘         └───────────┘
pid        └──┘└┘           └┘            └┘        └┘         └───────────┘
st   ────────────────────────────────────────────────────────────────────────┘└─
539    congr' 2,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid          
st   ─────────┘└─
540    { apply mul_comm },
id             └──────┘
src      └────┘└──────┘
typ      └────┘└──────┘
doc      └────┘        
txt      └────┘        
par      └────┘        
pid                   
st   ───┘└─────────────┘└┘
541    { rw [div_mul_eq_mul_div, mul_inv_cancel hw, one_div_eq_inv] }
id           └────────────────┘  └────────────┘ └┘  └────────────┘
src      └──┘└────────────────┘└┘└────────────┘  └┘└────────────┘└┘
typ      └──┘└────────────────┘└┘└────────────┘└┘└┘└────────────┘└┘
doc      └──┘                  └┘                └┘              └┘
txt      └──┘                  └┘                └┘              └┘
par      └──┘                  └┘                └┘              └┘
pid        └┘                  └┘                └┘              
st   ─────────────────────────┘└─────────────────┘└──────────────┘└─
542  end
st   ──┘
543  
544  lemma finset.center_mass_singleton (hw : w i ≠ 0) : (finset.singleton i).center_mass w z = z i :=
id                                                     └──────────────┘  └─────────┘      
src                                                      └──────────────┘   └─────────┘      
typ                                                    └──────────────┘  └─────────┘      
doc                                                       └──────────────┘   └─────────┘
545  by rw [center_mass, sum_singleton, sum_singleton, ← mul_smul, inv_mul_cancel hw, one_smul]
id          └─────────┘  └───────────┘  └───────────┘    └──────┘  └────────────┘ └┘  └──────┘
src     └──┘└─────────┘└┘└───────────┘└┘└───────────┘└──┘└──────┘└┘└────────────┘  └┘└──────┘└─
typ     └──┘└─────────┘└┘└───────────┘└┘└───────────┘└──┘└──────┘└┘└────────────┘└┘└┘└──────┘└─
doc     └──┘└─────────┘└┘             └┘             └──┘        └┘                └┘        └─
txt     └──┘           └┘             └┘             └──┘        └┘                └┘        └─
par     └──┘           └┘             └┘             └──┘        └┘                └┘        └─
pid       └┘           └┘             └┘             └──┘        └┘                └┘        
st     └──────────────┘└─────────────┘└─────────────┘└──────────┘└─────────────────┘└────────┘
546  
src  
typ  
doc  
txt  
par  
pid  
st   
547  lemma finset.center_mass_eq_of_sum_1 (hw : t.sum w = 1) :
id                                              └──┘  
src                                              └──┘   
typ                                             └──┘  
548    t.center_mass w z = t.sum (λ i, w i • z i) :=
id     └──────────┘    └──┘          
src     └──────────┘       └──┘           
typ    └──────────┘    └──┘          
doc     └──────────┘
549  by simp only [finset.center_mass, hw, inv_one, one_smul]
id                 └────────────────┘  └┘  └─────┘  └──────┘
src     └─────────┘└────────────────┘└┘  └┘└─────┘└┘└──────┘└─
typ     └─────────┘└────────────────┘└┘└┘└┘└─────┘└┘└──────┘└─
doc     └─────────┘└────────────────┘└┘  └┘       └┘        └─
txt     └─────────┘                  └┘  └┘       └┘        └─
par     └─────────┘                  └┘  └┘       └┘        └─
pid         └──┘└┘                  └┘  └┘       └┘        
st     └──────────────────────────────────────────────────────
550  
src  
typ  
doc  
txt  
par  
pid  
st   
551  lemma finset.center_mass_smul : t.center_mass w (λ i, c • z i) = c • t.center_mass w z :=
id                                   └──────────┘               └──────────┘  
src                                   └──────────┘                      └──────────┘
typ                                  └──────────┘               └──────────┘  
doc                                   └──────────┘                         └──────────┘
552  by simp only [finset.center_mass, finset.smul_sum, (mul_smul _ _ _).symm, mul_comm c, mul_assoc]
id                 └────────────────┘  └─────────────┘   └──────┘              └──────┘   └───────┘
src     └─────────┘└────────────────┘└┘└─────────────┘└┘ └──────┘└────────────┘└──────┘ └┘└───────┘└─
typ     └─────────┘└────────────────┘└┘└─────────────┘└┘ └──────┘└────────────┘└──────┘└┘└───────┘└─
doc     └─────────┘└────────────────┘└┘               └┘         └────────────┘         └┘         └─
txt     └─────────┘                  └┘               └┘         └────────────┘         └┘         └─
par     └─────────┘                  └┘               └┘         └────────────┘         └┘         └─
pid         └──┘└┘                  └┘               └┘         └────────────┘         └┘         
st     └──────────────────────────────────────────────────────────────────────────────────────────────
553  
src  
typ  
doc  
txt  
par  
pid  
st   
554  /-- A convex combination of two centers of mass is a center of mass as well. This version
555  deals with two different index types. -/
556  lemma finset.center_mass_segment'
557    (s : finset ι) (t : finset ι') (ws : ι → ℝ) (zs : ι → E) (wt : ι' → ℝ) (zt : ι' → E)
id          └────┘        └────┘ └┘                              └┘           └┘   
src         └────┘         └────┘                                         
typ         └────┘        └────┘ └┘                              └┘           └┘   
doc         └────┘         └────┘
558    (hws : s.sum ws = 1) (hwt : t.sum wt = 1) (a b : ℝ) (hab : a + b = 1):
id            └──┘ └┘            └──┘ └┘                        
src            └──┘                └──┘                             
typ           └──┘ └┘            └──┘ └┘                        
559    a • s.center_mass ws zs + b • t.center_mass wt zt =
id       └──────────┘ └┘ └┘    └──────────┘ └┘ └┘ 
src        └──────────┘            └──────────┘       
typ      └──────────┘ └┘ └┘    └──────────┘ └┘ └┘ 
doc         └──────────┘              └──────────┘
560      (s.image sum.inl ∪ t.image sum.inr).center_mass
id        └────┘ └─────┘  └────┘ └─────┘ └─────────┘
src        └────┘ └─────┘   └────┘ └─────┘ └─────────┘
typ       └────┘ └─────┘  └────┘ └─────┘ └─────────┘
doc        └────┘            └────┘         └─────────┘
561        (sum.elim (λ i, a * ws i) (λ j, b * wt j))
id          └──────┘        └┘          └┘ 
src         └──────┘                        
typ         └──────┘        └┘          └┘ 
562        (sum.elim zs zt) :=
id          └──────┘ └┘ └┘
src         └──────┘
typ         └──────┘ └┘ └┘
563  begin
st   └─────
564    rw [s.center_mass_eq_of_sum_1 _ hws, t.center_mass_eq_of_sum_1 _ hwt,
id         └───────────────────────┘   └─┘  └───────────────────────┘   └─┘
src    └──┘└───────────────────────┘└─┘   └┘└───────────────────────┘└─┘   └─
typ    └──┘└───────────────────────┘└─┘└─┘└┘└───────────────────────┘└─┘└─┘└─
doc    └──┘                         └─┘   └┘                         └─┘   └─
txt    └──┘                         └─┘   └┘                         └─┘   └─
par    └──┘                         └─┘   └┘                         └─┘   └─
pid      └┘                         └─┘   └┘                         └─┘   └─
st   ────────────────────────────────────┘└───────────────────────────────┘└─
565      smul_sum, smul_sum, ← finset.sum_sum_elim, finset.center_mass_eq_of_sum_1],
id       └──────┘  └──────┘    └─────────────────┘  └────────────────────────────┘
src  ───┘└──────┘└┘└──────┘└──┘└─────────────────┘└┘└────────────────────────────┘
typ  ───┘└──────┘└┘└──────┘└──┘└─────────────────┘└┘└────────────────────────────┘
doc  ───┘        └┘        └──┘                   └┘                              
txt  ───┘        └┘        └──┘                   └┘                              
par  ───┘        └┘        └──┘                   └┘                              
pid  ───┘        └┘        └──┘                   └┘                              
st   ───────────┘└────────┘└─────────────────────┘└──────────────────────────────┘└──
566    { congr, ext i, cases i; simp only [sum.elim_inl, sum.elim_inr, mul_smul] },
id                                        └──────────┘  └──────────┘  └──────┘
src      └───┘  └───┘  └────┘   └─────────┘└──────────┘└┘└──────────┘└┘└──────┘└┘
typ      └───┘  └───┘  └────┘  └─────────┘└──────────┘└┘└──────────┘└┘└──────┘└┘
doc             └───┘  └────┘   └─────────┘            └┘            └┘        └┘
txt      └───┘  └───┘  └────┘   └─────────┘            └┘            └┘        └┘
par      └───┘  └───┘  └────┘   └─────────┘            └┘            └┘        └┘
pid                └┘              └──┘└┘            └┘            └┘        
st   ───┘└───┘└─────┘└──────────────────────────────────────────────────────────┘└┘
567    { rw [sum_sum_elim, ← mul_sum, ← mul_sum, hws, hwt, mul_one, mul_one, hab] }
id           └──────────┘    └─────┘    └─────┘  └─┘  └─┘  └─────┘  └─────┘  └─┘
src      └──┘└──────────┘└──┘└─────┘└──┘└─────┘└┘   └┘   └┘└─────┘└┘└─────┘└┘   └┘
typ      └──┘└──────────┘└──┘└─────┘└──┘└─────┘└┘└─┘└┘└─┘└┘└─────┘└┘└─────┘└┘└─┘└┘
doc      └──┘            └──┘       └──┘       └┘   └┘   └┘       └┘       └┘   └┘
txt      └──┘            └──┘       └──┘       └┘   └┘   └┘       └┘       └┘   └┘
par      └──┘            └──┘       └──┘       └┘   └┘   └┘       └┘       └┘   └┘
pid        └┘            └──┘       └──┘       └┘   └┘   └┘       └┘       └┘   
st   ───────────────────┘└─────────┘└─────────┘└───┘└───┘└───────┘└───────┘└───┘└─
568  end
st   ──┘
569  
570  /-- A convex combination of two centers of mass is a center of mass as well. This version
571  works if two centers of mass share the set of original points. -/
572  lemma finset.center_mass_segment
573    (s : finset ι) (w₁ w₂ : ι → ℝ) (z : ι → E)
id          └────┘                         
src         └────┘                 
typ         └────┘                         
doc         └────┘
574    (hw₁ : s.sum w₁ = 1) (hw₂ : s.sum w₂ = 1) (a b : ℝ) (hab : a + b = 1):
id            └──┘ └┘            └──┘ └┘                        
src            └──┘                └──┘                             
typ           └──┘ └┘            └──┘ └┘                        
575    a • s.center_mass w₁ z + b • s.center_mass w₂ z =
id       └──────────┘ └┘     └──────────┘ └┘  
src        └──────────┘           └──────────┘      
typ      └──────────┘ └┘     └──────────┘ └┘  
doc         └──────────┘             └──────────┘
576      s.center_mass (λ i, a * w₁ i + b * w₂ i) z :=
id       └──────────┘        └┘     └┘   
src       └──────────┘                  
typ      └──────────┘        └┘     └┘   
doc       └──────────┘
577  have hw : s.sum (λ i, a * w₁ i + b * w₂ i) = 1,
id             └──┘        └┘     └┘   
src             └──┘                         
typ            └──┘        └┘     └┘   
578    by simp only [mul_sum.symm, sum_add_distrib, mul_one, *],
id                                 └─────────────┘  └─────┘
src       └─────────┘            └┘└─────────────┘└┘└─────┘└──┘
typ       └─────────┘└──────────┘└┘└─────────────┘└┘└─────┘└──┘
doc       └─────────┘            └┘               └┘       └──┘
txt       └─────────┘            └┘               └┘       └──┘
par       └─────────┘            └┘               └┘       └──┘
pid           └──┘└┘            └┘               └┘       └──┘
st       └────────────────────────────────────────────────────┘
579  by simp only [finset.center_mass_eq_of_sum_1, smul_sum, sum_add_distrib, add_smul, mul_smul, *]
id                 └────────────────────────────┘  └──────┘  └─────────────┘  └──────┘  └──────┘
src     └─────────┘└────────────────────────────┘└┘└──────┘└┘└─────────────┘└┘└──────┘└┘└──────┘└────
typ     └─────────┘└────────────────────────────┘└┘└──────┘└┘└─────────────┘└┘└──────┘└┘└──────┘└────
doc     └─────────┘                              └┘        └┘               └┘        └┘        └────
txt     └─────────┘                              └┘        └┘               └┘        └┘        └────
par     └─────────┘                              └┘        └┘               └┘        └┘        └────
pid         └──┘└┘                              └┘        └┘               └┘        └┘        └──┘
st     └─────────────────────────────────────────────────────────────────────────────────────────────
580  
src  
typ  
doc  
txt  
par  
pid  
st   
581  lemma finset.center_mass_ite_eq (hi : i ∈ t) :
id                                           
src                                          
typ                                          
582    t.center_mass (λ j, if (i = j) then 1 else 0) z = z i :=
id     └──────────┘                                
src     └──────────┘                                  
typ    └──────────┘                                
doc     └──────────┘
583  begin
st   └─────
584    rw [finset.center_mass_eq_of_sum_1],
id         └────────────────────────────┘
src    └──┘└────────────────────────────┘
typ    └──┘└────────────────────────────┘
doc    └──┘                              
txt    └──┘                              
par    └──┘                              
pid      └┘                              
st   ───────────────────────────────────┘└──
585    transitivity t.sum (λ j, if (i = j) then z i else 0),
id                  └───┘                       
src    └───────────┘└───┘  └──┘     └─────┘  └──────┘
typ    └───────────┘└───┘  └──┘     └─────┘└──────┘
doc    └───────────┘       └──┘      └─────┘  └──────┘
txt    └───────────┘       └──┘      └─────┘  └──────┘
par    └───────────┘       └──┘      └─────┘  └──────┘
pid                       └──┘      └─────┘  └──────┘
st   ─────────────────────────────────────────────────────┘└─
586    { congr, ext i, split_ifs, exacts [h ▸ one_smul _ _, zero_smul _ _] },
id                                          └──────┘      └───────┘
src      └───┘  └───┘  └───────┘  └──────┘ └──────┘└────┘└───────┘└────┘
typ      └───┘  └───┘  └───────┘  └──────┘└──────┘└────┘└───────┘└────┘
doc             └───┘  └───────┘  └──────┘          └────┘         └────┘
txt      └───┘  └───┘  └───────┘  └──────┘          └────┘         └────┘
par      └───┘  └───┘  └───────┘  └──────┘          └────┘         └────┘
pid                └┘                   └┘          └────┘         └───┘
st   ───┘└───┘└─────┘└─────────┘└─────────────────────────────────────────┘└┘
587    { rw [sum_ite_eq, if_pos hi] },
id           └────────┘  └────┘ └┘
src      └──┘└────────┘└┘└────┘  └┘
typ      └──┘└────────┘└┘└────┘└┘└┘
doc      └──┘          └┘        └┘
txt      └──┘          └┘        └┘
par      └──┘          └┘        └┘
pid        └┘          └┘        
st   ───┘└────────────┘└─────────┘└┘
588    { rw [sum_ite_eq, if_pos hi] }
id           └────────┘  └────┘ └┘
src      └──┘└────────┘└┘└────┘  └┘
typ      └──┘└────────┘└┘└────┘└┘└┘
doc      └──┘          └┘        └┘
txt      └──┘          └┘        └┘
par      └──┘          └┘        └┘
pid        └┘          └┘        
st   ─────────────────┘└─────────┘└─
589  end
st   ──┘
590  
591  variables {t w}
592  
593  lemma finset.center_mass_subset {t' : finset ι} (ht : t ⊆ t')
id                                         └────┘           └┘
src                                        └────┘            
typ                                        └────┘           └┘
doc                                        └────┘
594    (h : ∀ i ∈ t', i ∉ t → w i = 0) :
id               └┘         
src                              
typ              └┘         
595    t.center_mass w z = t'.center_mass w z :=
id     └──────────┘    └┘└──────────┘  
src     └──────────┘        └──────────┘
typ    └──────────┘    └┘└──────────┘  
doc     └──────────┘         └──────────┘
596  begin
st   └─────
597    rw [center_mass, sum_subset ht h, smul_sum, center_mass, smul_sum],
id         └─────────┘  └────────┘ └┘   └──────┘  └─────────┘  └──────┘
src    └──┘└─────────┘└┘└────────┘   └┘└──────┘└┘└─────────┘└┘└──────┘
typ    └──┘└─────────┘└┘└────────┘└┘└┘└──────┘└┘└─────────┘└┘└──────┘
doc    └──┘└─────────┘└┘             └┘        └┘└─────────┘└┘        
txt    └──┘           └┘             └┘        └┘           └┘        
par    └──┘           └┘             └┘        └┘           └┘        
pid      └┘           └┘             └┘        └┘           └┘        
st   ────────────────┘└───────────────┘└────────┘└───────────┘└────────┘└──
598    apply sum_subset ht,
id           └────────┘ └┘
src    └────┘└────────┘
typ    └────┘└────────┘└┘
doc    └────┘          
txt    └────┘          
par    └────┘          
pid                   
st   ────────────────────┘└─
599    assume i hit' hit,
src    └───────────────┘
typ    └───────────────┘
doc    └───────────────┘
txt    └───────────────┘
par    └───────────────┘
pid    └───────────────┘
st   ──────────────────┘└─
600    rw [h i hit' hit, zero_smul, smul_zero]
id           └──┘ └─┘  └───────┘  └───────┘
src    └──┘         └┘└───────┘└┘└───────┘└┘
typ    └──┘└──┘└─┘└┘└───────┘└┘└───────┘└┘
doc    └──┘         └┘         └┘         └┘
txt    └──┘         └┘         └┘         └┘
par    └──┘         └┘         └┘         └┘
pid      └┘         └┘         └┘         
st   ─────────────────┘└─────────┘└─────────┘
601  end
st   └─┘
602  
603  lemma finset.center_mass_filter_ne_zero :
604    (t.filter (λ i, w i ≠ 0)).center_mass w z = t.center_mass w z :=
id      └─────┘            └─────────┘     └──────────┘  
src      └─────┘               └─────────┘        └──────────┘
typ     └─────┘            └─────────┘     └──────────┘  
doc      └─────┘                └─────────┘         └──────────┘
605  finset.center_mass_subset z (filter_subset _) $ λ i hit hit',
id   └───────────────────────┘   └───────────┘         └─┘ └──┘
src  └───────────────────────┘    └───────────┘
typ  └───────────────────────┘   └───────────┘         └─┘ └──┘
606  by simpa only [hit, mem_filter, true_and, ne.def, not_not] using hit'
id                  └─┘  └────────┘  └──────┘  └────┘  └─────┘        └──┘
src     └──────────┘   └┘└────────┘└┘└──────┘└┘└────┘└┘└─────┘└──────┘    
typ     └──────────┘└─┘└┘└────────┘└┘└──────┘└┘└────┘└┘└─────┘└──────┘└──┘
doc     └──────────┘   └┘          └┘        └┘      └┘       └──────┘    
txt     └──────────┘   └┘          └┘        └┘      └┘       └──────┘    
par     └──────────┘   └┘          └┘        └┘      └┘       └──────┘    
pid          └──┘└┘   └┘          └┘        └┘      └┘       └────┘    
st     └───────────────────────────────────────────────────────────────────
607  
src  
typ  
doc  
txt  
par  
pid  
st   
608  variable {z}
609  
610  /-- Center mass of a finite subset of a convex set belongs to the set
611  provided that all weights are non-negative, and the total weight is positive. -/
612  lemma convex.center_mass_mem (hs : convex s) :
id                                      └────┘ 
src                                     └────┘
typ                                     └────┘ 
doc                                     └────┘
613    (∀ i ∈ t, 0 ≤ w i) → (0 < t.sum w) → (∀ i ∈ t, z i ∈ s) → t.center_mass w z ∈ s :=
id                         └──┘                    └──────────┘    
src                             └──┘                           └──────────┘     
typ                        └──┘                    └──────────┘    
doc                                                               └──────────┘
614  begin
st   └─────
615    refine finset.induction (by simp [lt_irrefl]) (λ i t hi ht h₀ hpos hmem, _) t,
id            └──────────────┘           └───────┘                                 
src    └─────┘└──────────────┘   └────┘└───────┘└┘  └──────────────────────────┘
typ    └─────┘└──────────────┘   └────┘└───────┘└┘  └──────────────────────────┘
doc    └─────┘                   └────┘         └┘  └──────────────────────────┘
txt    └─────┘                   └────┘         └┘  └──────────────────────────┘
par    └─────┘                   └────┘         └┘  └──────────────────────────┘
pid                             └─────┘         └─┘  └──────────────────────────┘
st   ────────────────────────────┘└───────────────┘└───────────────────────────────┘└─
616    have zi : z i ∈ s, from hmem _ (mem_insert_self _ _),
id                         └──┘    └─────────────┘
src    └────────┘     └───┘    └─┘ └─────────────┘└───┘
typ    └────────┘  └───┘└──┘└─┘ └─────────────┘└───┘
doc    └────────┘      └───┘    └─┘                └───┘
txt    └────────┘      └───┘    └─┘                └───┘
par    └────────┘      └───┘    └─┘                └───┘
pid    └─────┘└─┘      └───┘    └─┘                └───┘
st   ──────────────────┘└─────────────────────────────────┘└─
617    have hs₀ : ∀ j ∈ t, 0 ≤ w j, from λ j hj, h₀ j $ mem_insert_of_mem hj,
id                                            └┘     └───────────────┘
src    └─────────┘ └───┘  └─┘    └───┘ └─────┘    └───────────────┘
typ    └─────────┘ └───┘ └─┘   └───┘ └─────┘└┘  └───────────────┘
doc    └─────────┘ └───┘  └─┘     └───┘ └─────┘                     
txt    └─────────┘ └───┘  └─┘     └───┘ └─────┘                     
par    └─────────┘ └───┘  └─┘     └───┘ └─────┘                     
pid    └──────┘└─┘ └───┘  └─┘     └───┘ └─────┘                     
st   ────────────────────────────┘└────────────────────────────────────────┘└─
618    rw [sum_insert hi] at hpos,
id         └────────┘ └┘
src    └──┘└────────┘  └───────┘
typ    └──┘└────────┘└┘└───────┘
doc    └──┘            └───────┘
txt    └──┘            └───────┘
par    └──┘            └───────┘
pid      └┘            └──────┘
st   ──────────────────┘└──────┘└─
619    by_cases hsum_t : t.sum w = 0,
id                       └───┘  
src    └───────┘      └─┘└───┘ └┘
typ    └───────┘      └─┘└───┘└┘
doc    └───────┘      └─┘       └┘
txt    └───────┘      └─┘       └┘
par    └───────┘      └─┘       └┘
pid                  └─┘       
st   ──────────────────────────────┘└─
620    { have ws : ∀ j ∈ t, w j = 0, from (sum_eq_zero_iff_of_nonneg hs₀).1 hsum_t,
id                                       └───────────────────────┘ └─┘    └────┘
src      └────────┘ └───┘     └┘  └───┘ └───────────────────────┘   └──┘
typ      └────────┘ └───┘   └┘  └───┘ └───────────────────────┘└─┘└──┘└────┘
doc      └────────┘ └───┘     └┘  └───┘                             └──┘
txt      └────────┘ └───┘     └┘  └───┘                             └──┘
par      └────────┘ └───┘     └┘  └───┘                             └──┘
pid      └─────┘└─┘ └───┘       └───┘                             └──┘
st   ───┘└────────────────────────┘└─────────────────────────────────────────────┘└─
621      have wz : t.sum (λ j, w j • z j) = 0, from sum_eq_zero (λ i hi, by simp [ws i hi]),
id                 └───┘                         └─────────┘                   └┘  └┘
src      └────────┘└───┘  └──┘    └┘ └┘  └───┘└─────────┘  └─────┘  └────┘     
typ      └────────┘└───┘  └──┘  └┘ └┘  └───┘└─────────┘  └─────┘  └────┘└┘└┘
doc      └────────┘       └──┘     └┘ └┘  └───┘             └─────┘  └────┘     
txt      └────────┘       └──┘     └┘ └┘  └───┘             └─────┘  └────┘     
par      └────────┘       └──┘     └┘ └┘  └───┘             └─────┘  └────┘     
pid      └─────┘└─┘       └──┘     └┘   └───┘             └─────┘  └─────┘     └┘
st   ───────────────────────────────────────┘└────────────────────────────┘└─────────────┘└─
622      simp only [center_mass, sum_insert hi, wz, hsum_t, add_zero],
id                  └─────────┘  └────────┘ └┘  └┘  └────┘  └──────┘
src      └─────────┘└─────────┘└┘└────────┘  └┘  └┘      └┘└──────┘
typ      └─────────┘└─────────┘└┘└────────┘└┘└┘└┘└┘└────┘└┘└──────┘
doc      └─────────┘└─────────┘└┘            └┘  └┘      └┘        
txt      └─────────┘           └┘            └┘  └┘      └┘        
par      └─────────┘           └┘            └┘  └┘      └┘        
pid          └──┘└┘           └┘            └┘  └┘      └┘        
st   ───────────────────────────────────────────────────────────────┘└─
623      simp only [hsum_t, add_zero] at hpos,
id                  └────┘  └──────┘
src      └─────────┘      └┘└──────┘└───────┘
typ      └─────────┘└────┘└┘└──────┘└───────┘
doc      └─────────┘      └┘        └───────┘
txt      └─────────┘      └┘        └───────┘
par      └─────────┘      └┘        └───────┘
pid          └──┘└┘      └┘        └─────┘
st   ───────────────────────────────────────┘└─
624      rw [← mul_smul, inv_mul_cancel (ne_of_gt hpos), one_smul],
id             └──────┘  └────────────┘  └──────┘ └──┘   └──────┘
src      └────┘└──────┘└┘└────────────┘ └──────┘    └─┘└──────┘
typ      └────┘└──────┘└┘└────────────┘ └──────┘└──┘└─┘└──────┘
doc      └────┘        └┘                           └─┘        
txt      └────┘        └┘                           └─┘        
par      └────┘        └┘                           └─┘        
pid        └──┘        └┘                           └─┘        
st   ─────────────────┘└──────────────────────────────┘└────────┘└──
625      exact zi },
id             └┘
src      └────┘  
typ      └────┘└┘
doc      └────┘  
txt      └────┘  
par      └────┘  
pid             
st   ────────────┘└┘
626    { rw [finset.center_mass_insert _ _ _ hi hsum_t],
id           └───────────────────────┘       └┘ └────┘
src      └──┘└───────────────────────┘└─────┘        
typ      └──┘└───────────────────────┘└─────┘└┘└────┘
doc      └──┘                         └─────┘        
txt      └──┘                         └─────┘        
par      └──┘                         └─────┘        
pid        └┘                         └─────┘        
st   ────────────────────────────────────────────────┘└──
627      refine convex_iff_div.1 hs zi (ht hs₀ _ _) _ (sum_nonneg hs₀) hpos,
id              └────────────┘   └┘ └┘  └┘             └────────┘ └─┘  └──┘
src      └─────┘└────────────┘└─┘          └──────┘ └────────┘   └┘
typ      └─────┘└────────────┘└─┘└┘└┘ └┘   └──────┘ └────────┘└─┘└┘└──┘
doc      └─────┘└────────────┘└─┘          └──────┘              └┘
txt      └─────┘              └─┘          └──────┘              └┘
par      └─────┘              └─┘          └──────┘              └┘
pid                          └─┘          └──────┘              └┘
st   ─────────────────────────────────────────────────────────────────────┘└─
628      { exact lt_of_le_of_ne (sum_nonneg hs₀) (ne.symm hsum_t) },
id               └────────────┘  └────────┘ └─┘   └─────┘ └────┘
src        └────┘└────────────┘ └────────┘   └┘ └─────┘      └┘
typ        └────┘└────────────┘ └────────┘└─┘└┘ └─────┘└────┘└┘
doc        └────┘                            └┘              └┘
txt        └────┘                            └┘              └┘
par        └────┘                            └┘              └┘
pid                                         └┘              
st   ─────┘└─────────────────────────────────────────────────────┘└┘
629      { intros j hj, exact hmem j (mem_insert_of_mem hj) },
id                            └──┘   └───────────────┘ └┘
src        └─────────┘  └────┘      └───────────────┘  └┘
typ        └─────────┘  └────┘└──┘ └───────────────┘└┘└┘
doc        └─────────┘  └────┘                         └┘
txt        └─────────┘  └────┘                         └┘
par        └─────────┘  └────┘                         └┘
pid              └───┘                                
st   ─────┘└─────────┘└────────────────────────────────────┘└┘
630      { exact h₀ _ (mem_insert_self _ _) } }
id               └┘    └─────────────┘
src        └────┘  └─┘ └─────────────┘└────┘
typ        └────┘└┘└─┘ └─────────────┘└────┘
doc        └────┘  └─┘                └────┘
txt        └────┘  └─┘                └────┘
par        └────┘  └─┘                └────┘
pid               └─┘                └───┘
st   ──────────────────────────────────────┘└───
631  end
st   ──┘
632  
633  lemma convex.sum_mem (hs : convex s) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : t.sum w = 1)
id                              └────┘                            └──┘  
src                             └────┘                                  └──┘   
typ                             └────┘                            └──┘  
doc                             └────┘
634    (hz : ∀ i ∈ t, z i ∈ s) :
id                     
src                       
typ                    
635    t.sum (λ i, w i • z i) ∈ s :=
id     └──┘             
src     └──┘                 
typ    └──┘             
636  by simpa only [h₁, center_mass, inv_one, one_smul] using
id                  └┘  └─────────┘  └─────┘  └──────┘
src     └──────────┘  └┘└─────────┘└┘└─────┘└┘└──────┘└───────
typ     └──────────┘└┘└┘└─────────┘└┘└─────┘└┘└──────┘└───────
doc     └──────────┘  └┘└─────────┘└┘       └┘        └───────
txt     └──────────┘  └┘           └┘       └┘        └───────
par     └──────────┘  └┘           └┘       └┘        └───────
pid          └──┘└┘  └┘           └┘       └┘        └─────
st     └──────────────────────────────────────────────────────
637    hs.center_mass_mem h₀ (h₁.symm ▸ zero_lt_one) hz
id     └────────────────┘ └┘  └─────┘  └─────────┘  └┘
src  ─┘└────────────────┘   └─────┘└─────────┘└┘  
typ  ─┘└────────────────┘└┘ └─────┘└─────────┘└┘└┘
doc  ─┘└────────────────┘                      └┘  
txt  ─┘                                        └┘  
par  ─┘                                        └┘  
pid  ─┘                                        └┘  
st   ───────────────────────────────────────────────────
638  
src  
typ  
doc  
txt  
par  
pid  
st   
639  lemma convex_iff_sum_mem :
640    convex s ↔
id     └────┘  
src    └────┘   
typ    └────┘  
doc    └────┘
641      (∀ (t : finset E) (w : E → ℝ),
id               └────┘          
src              └────┘             
typ              └────┘          
doc              └────┘
642        (∀ i ∈ t, 0 ≤ w i) → t.sum w = 1 → (∀ x ∈ t, x ∈ s) → t.sum (λx, w x • x) ∈ s ) :=
id                         └──┘                     └──┘           
src                             └──┘                           └──┘              
typ                        └──┘                     └──┘           
643  begin
st   └─────
644    refine ⟨λ hs t w hw₀ hw₁ hts, hs.sum_mem hw₀ hw₁ hts, _⟩,
id                                     └──────┘
src    └─────┘  └───────────────────┘  └──────┘         └──┘
typ    └─────┘  └───────────────────┘  └──────┘         └──┘
doc    └─────┘  └───────────────────┘                   └──┘
txt    └─────┘  └───────────────────┘                   └──┘
par    └─────┘  └───────────────────┘                   └──┘
pid            └───────────────────┘                   └──┘
st   ─────────────────────────────────────────────────────────┘└─
645    intros h x y hx hy a b ha hb hab,
src    └──────────────────────────────┘
typ    └──────────────────────────────┘
doc    └──────────────────────────────┘
txt    └──────────────────────────────┘
par    └──────────────────────────────┘
pid          └────────────────────────┘
st   ─────────────────────────────────┘└─
646    by_cases h_cases: x = y,
id                         
src    └───────┘       └┘ 
typ    └───────┘       └┘
doc    └───────┘       └┘  
txt    └───────┘       └┘  
par    └───────┘       └┘  
pid                   └┘  
st   ────────────────────────┘└─
647    { rw [h_cases, ←add_smul, hab, one_smul], exact hy },
id           └─────┘   └──────┘  └─┘  └──────┘         └┘
src      └──┘       └─┘└──────┘└┘   └┘└──────┘  └────┘  
typ      └──┘└─────┘└─┘└──────┘└┘└─┘└┘└──────┘  └────┘└┘
doc      └──┘       └─┘        └┘   └┘          └────┘  
txt      └──┘       └─┘        └┘   └┘          └────┘  
par      └──┘       └─┘        └┘   └┘          └────┘  
pid        └┘       └─┘        └┘   └┘                 
st   ───┘└─────────┘└─────────┘└───┘└────────┘└──────────┘└┘
648    { convert h {x, y} (λ z, if z = y then b else a) _ _ _,
id                                               
src      └──────┘ └─┘ └┘  └──┘  └─┘  └────┘ └────┘ └─────┘
typ      └──────┘└─┘ └┘  └──┘  └─┘ └────┘└────┘└─────┘
doc      └──────┘  └─┘ └┘  └──┘  └─┘  └────┘ └────┘ └─────┘
txt      └──────┘  └─┘ └┘  └──┘  └─┘  └────┘ └────┘ └─────┘
par      └──────┘  └─┘ └┘  └──┘  └─┘  └────┘ └────┘ └─────┘
pid               └─┘ └┘  └──┘  └─┘  └────┘ └────┘ └─────┘
st   ───────────────────────────────────────────────────────┘└─
649      { simp only [sum_pair h_cases, if_neg h_cases, if_pos rfl] },
id                    └──────┘ └─────┘  └────┘ └─────┘  └────┘ └─┘
src        └─────────┘└──────┘       └┘└────┘       └┘└────┘└─┘└┘
typ        └─────────┘└──────┘└─────┘└┘└────┘└─────┘└┘└────┘└─┘└┘
doc        └─────────┘               └┘             └┘         └┘
txt        └─────────┘               └┘             └┘         └┘
par        └─────────┘               └┘             └┘         └┘
pid            └──┘└┘               └┘             └┘         
st   ─────┘└───────────────────────────────────────────────────────┘└┘
650      { simp_intros i hi,
src        └──────────────┘
typ        └──────────────┘
doc        └──────────────┘
txt        └──────────────┘
par        └──────────────┘
pid                   └───┘
st   ─────┘└──────────────┘└─
651        cases hi; subst i; simp [ha, hb, if_neg h_cases] },
id               └┘                └┘  └┘  └────┘ └─────┘
src        └────┘    └────┘   └────┘  └┘  └┘└────┘       └┘
typ        └────┘└┘  └────┘  └────┘└┘└┘└┘└┘└────┘└─────┘└┘
doc        └────┘    └────┘   └────┘  └┘  └┘             └┘
txt        └────┘    └────┘   └────┘  └┘  └┘             └┘
par        └────┘    └────┘   └────┘  └┘  └┘             └┘
pid                               └┘  └┘             
st   ──────────────────────────────────────────────────────┘└┘
652      { simp only [sum_pair h_cases, if_neg h_cases, if_pos rfl, hab] },
id                    └──────┘ └─────┘  └────┘ └─────┘  └────┘ └─┘  └─┘
src        └─────────┘└──────┘       └┘└────┘       └┘└────┘└─┘└┘   └┘
typ        └─────────┘└──────┘└─────┘└┘└────┘└─────┘└┘└────┘└─┘└┘└─┘└┘
doc        └─────────┘               └┘             └┘         └┘   └┘
txt        └─────────┘               └┘             └┘         └┘   └┘
par        └─────────┘               └┘             └┘         └┘   └┘
pid            └──┘└┘               └┘             └┘         └┘   
st   ─────┘└────────────────────────────────────────────────────────────┘└┘
653      { simp_intros i hi,
src        └──────────────┘
typ        └──────────────┘
doc        └──────────────┘
txt        └──────────────┘
par        └──────────────┘
pid                   └───┘
st   ─────────────────────┘└─
654        cases hi; subst i; simp [hx, hy, if_neg h_cases] } }
id               └┘                └┘  └┘  └────┘ └─────┘
src        └────┘    └────┘   └────┘  └┘  └┘└────┘       └┘
typ        └────┘└┘  └────┘  └────┘└┘└┘└┘└┘└────┘└─────┘└┘
doc        └────┘    └────┘   └────┘  └┘  └┘             └┘
txt        └────┘    └────┘   └────┘  └┘  └┘             └┘
par        └────┘    └────┘   └────┘  └┘  └┘             └┘
pid                               └┘  └┘             
st   ──────────────────────────────────────────────────────┘└───
655  end
st   ──┘
656  
657  /-- Jensen's inequality, `finset.center_mass` version. -/
658  lemma convex_on.map_center_mass_le {f : E → ℝ} (hf : convex_on s f)
id                                                      └───────┘  
src                                                      └───────┘
typ                                                     └───────┘  
doc                                                       └───────┘
659    (h₀ : ∀ i ∈ t, 0 ≤ w i) (hpos : 0 < t.sum w)
id                                   └──┘ 
src                                       └──┘
typ                                  └──┘ 
660    (hmem : ∀ i ∈ t, z i ∈ s) : f (t.center_mass w z) ≤ t.center_mass w (f ∘ z) :=
id                             └──────────┘     └──────────┘     
src                                   └──────────┘        └──────────┘      
typ                            └──────────┘     └──────────┘     
doc                                    └──────────┘         └──────────┘
661  begin
st   └─────
662    have hmem' : ∀ i ∈ t, (z i, (f ∘ z) i) ∈ {p : E × ℝ | p.1 ∈ s ∧ f p.1 ≤ p.2},
id                                                                 
src    └───────────┘ └───┘    └┘   └┘ └┘ └──┘  └─┘ └─┘    └─┘ └─┘
typ    └───────────┘ └───┘   └┘  └┘ └┘ └──┘ └─┘ └─┘  └─┘ └─┘
doc    └───────────┘ └───┘     └┘    └┘ └┘  └──┘   └─┘ └─┘     └─┘  └─┘
txt    └───────────┘ └───┘     └┘    └┘ └┘  └──┘   └─┘ └─┘     └─┘  └─┘
par    └───────────┘ └───┘     └┘    └┘ └┘  └──┘   └─┘ └─┘     └─┘  └─┘
pid    └────────┘└─┘ └───┘     └┘    └┘ └┘  └──┘   └─┘ └─┘     └─┘  └─┘
st   ─────────────────────────────────────────────────────────────────────────────┘└─
663      from λ i hi, ⟨hmem i hi, le_refl _⟩,
id                     └──┘       └─────┘
src      └───┘ └─────┘        └┘└─────┘└─┘
typ      └───┘ └─────┘ └──┘   └┘└─────┘└─┘
doc      └───┘ └─────┘        └┘       └─┘
txt      └───┘ └─────┘        └┘       └─┘
par      └───┘ └─────┘        └┘       └─┘
pid      └───┘ └─────┘        └┘       └─┘
st   ──────────────────────────────────────┘└─
664    convert (hf.convex_epigraph.center_mass_mem h₀ hpos hmem').2;
id              └────────────────────────────────┘ └┘ └──┘ └───┘
src    └──────┘ └────────────────────────────────┘           └─┘
typ    └──────┘ └────────────────────────────────┘└┘└──┘└───┘└─┘
doc    └──────┘ └────────────────────────────────┘           └─┘
txt    └──────┘                                              └─┘
par    └──────┘                                              └─┘
pid                                                         └┘
st   ────────────────────────────────────────────────────────────────
665      simp only [center_mass, function.comp, prod.smul_fst, prod.fst_sum, prod.smul_snd, prod.snd_sum]
id                  └─────────┘  └───────────┘  └───────────┘  └──────────┘  └───────────┘  └──────────┘
src      └─────────┘└─────────┘└┘└───────────┘└┘└───────────┘└┘└──────────┘└┘└───────────┘└┘└──────────┘└┘
typ      └─────────┘└─────────┘└┘└───────────┘└┘└───────────┘└┘└──────────┘└┘└───────────┘└┘└──────────┘└┘
doc      └─────────┘└─────────┘└┘             └┘             └┘            └┘             └┘            └┘
txt      └─────────┘           └┘             └┘             └┘            └┘             └┘            └┘
par      └─────────┘           └┘             └┘             └┘            └┘             └┘            └┘
pid          └──┘└┘           └┘             └┘             └┘            └┘             └┘            
st   ────────────────────────────────────────────────────────────────────────────────────────────────────┘
666  end
st   └─┘
667  
668  /-- Jensen's inequality, `finset.sum` version. -/
669  lemma convex_on.map_sum_le {f : E → ℝ} (hf : convex_on s f)
id                                              └───────┘  
src                                              └───────┘
typ                                             └───────┘  
doc                                               └───────┘
670    (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : t.sum w = 1)
id                              └──┘  
src                                  └──┘   
typ                             └──┘  
671    (hmem : ∀ i ∈ t, z i ∈ s) : f (t.sum (λ i, w i • z i)) ≤ t.sum (λ i, w i * (f (z i))) :=
id                             └──┘              └──┘             
src                                   └──┘                    └──┘           
typ                            └──┘              └──┘             
672  by simpa only [center_mass, h₁, inv_one, one_smul]
id                  └─────────┘  └┘  └─────┘  └──────┘
src     └──────────┘└─────────┘└┘  └┘└─────┘└┘└──────┘└─
typ     └──────────┘└─────────┘└┘└┘└┘└─────┘└┘└──────┘└─
doc     └──────────┘└─────────┘└┘  └┘       └┘        └─
txt     └──────────┘           └┘  └┘       └┘        └─
par     └──────────┘           └┘  └┘       └┘        └─
pid          └──┘└┘           └┘  └┘       └┘        
st     └────────────────────────────────────────────────
673    using hf.map_center_mass_le h₀ (h₁.symm ▸ zero_lt_one) hmem
id           └───────────────────┘ └┘  └─────┘  └─────────┘  └──┘
src  ───────┘└───────────────────┘   └─────┘└─────────┘└┘    
typ  ───────┘└───────────────────┘└┘ └─────┘└─────────┘└┘└──┘
doc  ───────┘└───────────────────┘                      └┘    
txt  ───────┘                                           └┘    
par  ───────┘                                           └┘    
pid  ─┘└────┘                                           └┘    
st   ──────────────────────────────────────────────────────────────
674  
src  
typ  
doc  
txt  
par  
pid  
st   
675  /-- If a function `f` is convex on `s` takes value `y` at the center mass of some points
676  `z i ∈ s`, then for some `i` we have `y ≤ f (z i)`. -/
677  lemma convex_on.exists_ge_of_center_mass {f : E → ℝ} (h : convex_on s f)
id                                                           └───────┘  
src                                                           └───────┘
typ                                                          └───────┘  
doc                                                            └───────┘
678    (hw₀ : ∀ i ∈ t, 0 ≤ w i) (hws : 0 < t.sum w) (hz : ∀ i ∈ t, z i ∈ s) :
id                                   └──┘                   
src                                       └──┘                       
typ                                  └──┘                   
679    ∃ i ∈ t, f (t.center_mass w z) ≤ f (z i) :=
id            └──────────┘        
src               └──────────┘      
typ           └──────────┘        
doc                 └──────────┘
680  begin
st   └─────
681    set y := t.center_mass w z,
id              └───────────┘  
src    └───────┘└───────────┘ 
typ    └───────┘└───────────┘
doc    └───────┘└───────────┘ 
txt    └───────┘              
par    └───────┘              
pid       └┘              
st   ───────────────────────────┘└─
682    have : f y ≤ t.center_mass w (f ∘ z) := h.map_center_mass_le hw₀ hws hz,
id                └───────────┘          └──────────────────┘ └─┘ └─┘ └┘
src    └─────┘  └───────────┘    └───┘└──────────────────┘      
typ    └─────┘ └───────────┘ └───┘└──────────────────┘└─┘└─┘└┘
doc    └─────┘   └───────────┘     └───┘└──────────────────┘      
txt    └─────┘                     └───┘                          
par    └─────┘                     └───┘                          
pid    └───┘└┘                     └──┘                          
st   ────────────────────────────────────────────────────────────────────────┘└─
683    rw ← sum_filter_ne_zero at hws,
id          └────────────────┘
src    └───┘└────────────────┘└─────┘
typ    └───┘└────────────────┘└─────┘
doc    └───┘                  └─────┘
txt    └───┘                  └─────┘
par    └───┘                  └─────┘
pid      └─┘                  └─────┘
st   ───────────────────────────────┘└─
684    rw [← finset.center_mass_filter_ne_zero (f ∘ z), center_mass, smul_eq_mul,
id           └───────────────────────────────┘        └─────────┘  └─────────┘
src    └────┘└───────────────────────────────┘    └─┘└─────────┘└┘└─────────┘└─
typ    └────┘└───────────────────────────────┘  └─┘└─────────┘└┘└─────────┘└─
doc    └────┘                                     └─┘└─────────┘└┘           └─
txt    └────┘                                     └─┘           └┘           └─
par    └────┘                                     └─┘           └┘           └─
pid      └──┘                                     └─┘           └┘           └─
st   ────────────────────────────────────────────────┘└───────────┘└───────────┘└─
685      ← div_eq_inv_mul, le_div_iff hws, mul_sum] at this,
id         └────────────┘  └────────┘ └─┘  └─────┘
src  ─────┘└────────────┘└┘└────────┘   └┘└─────┘└───────┘
typ  ─────┘└────────────┘└┘└────────┘└─┘└┘└─────┘└───────┘
doc  ─────┘              └┘             └┘       └───────┘
txt  ─────┘              └┘             └┘       └───────┘
par  ─────┘              └┘             └┘       └───────┘
pid  ─────┘              └┘             └┘       └──────┘
st   ───────────────────┘└──────────────┘└───────┘└──────┘└─
686    replace : ∃ i ∈ t.filter (λ i, w i ≠ 0), f y * w i ≤ w i • (f ∘ z) i :=
id                    └──────┘                                 
src    └────────┘└───┘└──────┘  └──┘  └─┘           └┘ └───
typ    └────────┘└───┘└──────┘  └──┘  └─┘       └┘ └───
doc    └────────┘ └───┘└──────┘  └──┘   └─┘              └┘ └───
txt    └────────┘ └───┘          └──┘   └─┘              └┘ └───
par    └────────┘ └───┘          └──┘   └─┘              └┘ └───
pid           └┘ └───┘          └──┘   └─┘              └┘ └───
st   ──────────────────────────────────────────────────────────────────────────
687      exists_le_of_sum_le (nonempty_of_sum_ne_zero (ne_of_gt hws)) this,
id       └─────────────────┘  └─────────────────────┘  └──────┘ └─┘   └──┘
src  ───┘└─────────────────┘ └─────────────────────┘ └──────┘   └─┘
typ  ───┘└─────────────────┘ └─────────────────────┘ └──────┘└─┘└─┘└──┘
doc  ───┘                                                       └─┘
txt  ───┘                                                       └─┘
par  ───┘                                                       └─┘
pid  ───┘                                                       └─┘
st   ────────────────────────────────────────────────────────────────────┘└─
688    rcases this with ⟨i, hi, H⟩,
id            └──┘
src    └─────┘    └──────────────┘
typ    └─────┘└──┘└──────────────┘
doc    └─────┘    └──────────────┘
txt    └─────┘    └──────────────┘
par    └─────┘    └──────────────┘
pid              └──────────────┘
st   ────────────────────────────┘└─
689    rw [mem_filter] at hi,
id         └────────┘
src    └──┘└────────┘└─────┘
typ    └──┘└────────┘└─────┘
doc    └──┘          └─────┘
txt    └──┘          └─────┘
par    └──┘          └─────┘
pid      └┘          └────┘
st   ───────────────┘└────┘└─
690    use [i, hi.1],
id            └┘
src    └───┘ └┘  └─┘
typ    └───┘└┘└┘└─┘
doc    └───┘ └┘  └─┘
txt    └───┘ └┘  └─┘
par    └───┘ └┘  └─┘
pid       └┘ └┘  └─┘
st   ──────────────┘└─
691    simp only [smul_eq_mul, mul_comm (w i)] at H,
id                └─────────┘  └──────┘   
src    └─────────┘└─────────┘└┘└──────┘   └─────┘
typ    └─────────┘└─────────┘└┘└──────┘ └─────┘
doc    └─────────┘           └┘           └─────┘
txt    └─────────┘           └┘           └─────┘
par    └─────────┘           └┘           └─────┘
pid        └──┘└┘           └┘           └┘└──┘
st   ─────────────────────────────────────────────┘└─
692    refine (mul_le_mul_right _).1 H,
id             └──────────────┘      
src    └─────┘ └──────────────┘└────┘
typ    └─────┘ └──────────────┘└────┘
doc    └─────┘                 └────┘
txt    └─────┘                 └────┘
par    └─────┘                 └────┘
pid                           └────┘
st   ────────────────────────────────┘└─
693    exact lt_of_le_of_ne (hw₀ i hi.1) hi.2.symm
id           └────────────┘  └─┘        └┘
src    └────┘└────────────┘       └──┘  └──────┘
typ    └────┘└────────────┘ └─┘  └──┘└┘└──────┘
doc    └────┘                     └──┘  └──────┘
txt    └────┘                     └──┘  └──────┘
par    └────┘                     └──┘  └──────┘
pid                              └──┘  └────┘└┘
st   ─────────────────────────────────────────────┘
694  end
st   └─┘
695  
696  end center_mass
697  
698  section convex_hull
699  
700  variable {t : set E}
id                 └─┘
src                └─┘
typ                └─┘
701  
702  /-- Convex hull of a set `s` is the minimal convex set that includes `s` -/
703  def convex_hull (s : set E) : set E :=
id                        └─┘     └─┘ 
src                       └─┘      └─┘
typ                       └─┘     └─┘ 
704  ⋂ (t : set E) (hst : s ⊆ t) (ht : convex t), t
id         └─┘                    └────┘   
src        └─┘                       └────┘   
typ        └─┘                    └────┘   
doc                                   └────┘   
705  
706  variable (s)
707  
708  lemma subset_convex_hull : s ⊆ convex_hull s :=
id                                └─────────┘ 
src                                └─────────┘
typ                               └─────────┘ 
doc                                 └─────────┘
709  set.subset_Inter $ λ t, set.subset_Inter $ λ hst, set.subset_Inter $ λ ht, hst
id   └──────────────┘       └──────────────┘     └─┘  └──────────────┘     └┘  └─┘
src  └──────────────┘        └──────────────┘          └──────────────┘
typ  └──────────────┘       └──────────────┘     └─┘  └──────────────┘     └┘  └─┘
710  
711  lemma convex_convex_hull : convex (convex_hull s) :=
id                              └────┘  └─────────┘ 
src                             └────┘  └─────────┘
typ                             └────┘  └─────────┘ 
doc                             └────┘  └─────────┘
712  convex_Inter $ λ t, convex_Inter $ λ ht, convex_Inter id
id   └──────────┘       └──────────┘     └┘  └──────────┘ └┘
src  └──────────┘        └──────────┘         └──────────┘ └┘
typ  └──────────┘       └──────────┘     └┘  └──────────┘ └┘
713  
714  variable {s}
715  
716  lemma convex_hull_min (hst : s ⊆ t) (ht : convex t) : convex_hull s ⊆ t :=
id                                          └────┘     └─────────┘   
src                                           └────┘      └─────────┘   
typ                                         └────┘     └─────────┘   
doc                                            └────┘      └─────────┘
717  set.Inter_subset_of_subset t $ set.Inter_subset_of_subset hst $ set.Inter_subset _ ht
id   └────────────────────────┘    └────────────────────────┘ └─┘   └──────────────┘   └┘
src  └────────────────────────┘     └────────────────────────┘       └──────────────┘
typ  └────────────────────────┘    └────────────────────────┘ └─┘   └──────────────┘   └┘
718  
719  lemma convex_hull_mono (hst : s ⊆ t) : convex_hull s ⊆ convex_hull t :=
id                                       └─────────┘   └─────────┘ 
src                                        └─────────┘    └─────────┘
typ                                      └─────────┘   └─────────┘ 
doc                                         └─────────┘     └─────────┘
720  convex_hull_min (set.subset.trans hst $ subset_convex_hull t) (convex_convex_hull t)
id   └─────────────┘  └──────────────┘ └─┘   └────────────────┘    └────────────────┘ 
src  └─────────────┘  └──────────────┘       └────────────────┘     └────────────────┘
typ  └─────────────┘  └──────────────┘ └─┘   └────────────────┘    └────────────────┘ 
721  
722  lemma convex.convex_hull_eq {s : set E} (hs : convex s) : convex_hull s = s :=
id                                    └─┘         └────┘     └─────────┘   
src                                   └─┘          └────┘      └─────────┘   
typ                                   └─┘         └────┘     └─────────┘   
doc                                                └────┘      └─────────┘
723  set.subset.antisymm (convex_hull_min (set.subset.refl _) hs) (subset_convex_hull s)
id   └─────────────────┘  └─────────────┘  └─────────────┘    └┘   └────────────────┘ 
src  └─────────────────┘  └─────────────┘  └─────────────┘         └────────────────┘
typ  └─────────────────┘  └─────────────┘  └─────────────┘    └┘   └────────────────┘ 
724  
725  lemma is_linear_map.image_convex_hull {f : E → F} (hf : is_linear_map ℝ f) :
id                                                         └───────────┘  
src                                                          └───────────┘ 
typ                                                        └───────────┘  
726    f '' (convex_hull s) = convex_hull (f '' s) :=
id      └┘  └─────────┘    └─────────┘   └┘ 
src      └┘  └─────────┘     └─────────┘    └┘
typ     └┘  └─────────┘    └─────────┘   └┘ 
doc          └─────────┘      └─────────┘
727  begin
st   └─────
728    refine set.subset.antisymm _ _,
id            └─────────────────┘
src    └─────┘└─────────────────┘└──┘
typ    └─────┘└─────────────────┘└──┘
doc    └─────┘                   └──┘
txt    └─────┘                   └──┘
par    └─────┘                   └──┘
pid                             └──┘
st   ───────────────────────────────┘└─
729    { rw [set.image_subset_iff],
id           └──────────────────┘
src      └──┘└──────────────────┘
typ      └──┘└──────────────────┘
doc      └──┘└──────────────────┘
txt      └──┘                    
par      └──┘                    
pid        └┘                    
st   ───┘└──────────────────────┘└──
730      exact convex_hull_min (set.image_subset_iff.1 $ subset_convex_hull $ f '' s)
id             └─────────────┘  └──────────────────┘     └────────────────┘     └┘
src      └────┘└─────────────┘ └──────────────────┘└─┘ └────────────────┘  └┘ └─
typ      └────┘└─────────────┘ └──────────────────┘└─┘ └────────────────┘  └┘ └─
doc      └────┘                └──────────────────┘└─┘                        └─
txt      └────┘                                    └─┘                        └─
par      └────┘                                    └─┘                        └─
pid                                               └─┘                        └─
st   ─────────────────────────────────────────────────────────────────────────────────
731        ((convex_convex_hull (f '' s)).is_linear_preimage hf) },
id           └────────────────┘                            └┘
src  ─────┘  └────────────────┘     └────────────────────┘  └┘
typ  ─────┘  └────────────────┘   └────────────────────┘└┘└┘
doc  ─────┘                         └────────────────────┘  └┘
txt  ─────┘                         └────────────────────┘  └┘
par  ─────┘                         └────────────────────┘  └┘
pid  ─────┘                         └────────────────────┘  
st   ───────────────────────────────────────────────────────────┘└┘
732    { exact convex_hull_min (set.image_subset _ $ subset_convex_hull s)
id             └─────────────┘  └──────────────┘     └────────────────┘
src      └────┘└─────────────┘ └──────────────┘└─┘ └────────────────┘ └─
typ      └────┘└─────────────┘ └──────────────┘└─┘ └────────────────┘ └─
doc      └────┘                                └─┘                    └─
txt      └────┘                                └─┘                    └─
par      └────┘                                └─┘                    └─
pid                                           └─┘                    └─
st   ──────────────────────────────────────────────────────────────────────
733       ((convex_convex_hull s).is_linear_image hf) }
id          └────────────────┘                   └┘
src  ────┘  └────────────────┘ └────────────────┘  └┘
typ  ────┘  └────────────────┘└────────────────┘└┘└┘
doc  ────┘                     └────────────────┘  └┘
txt  ────┘                     └────────────────┘  └┘
par  ────┘                     └────────────────┘  └┘
pid  ────┘                     └────────────────┘  
st   ────────────────────────────────────────────────┘└─
734  end
st   ──┘
735  
736  lemma linear_map.image_convex_hull (f : E →ₗ[ℝ] F) :
id                                            └─┘ 
src                                            └─┘
typ                                           └─┘ 
737    f '' (convex_hull s) = convex_hull (f '' s) :=
id      └┘  └─────────┘    └─────────┘   └┘ 
src      └┘  └─────────┘     └─────────┘    └┘
typ     └┘  └─────────┘    └─────────┘   └┘ 
doc          └─────────┘      └─────────┘
738  f.is_linear.image_convex_hull
id   └────────┘└────────────────┘
src   └────────┘└────────────────┘
typ  └────────┘└────────────────┘
739  
740  lemma finset.center_mass_mem_convex_hull (t : finset ι) {w : ι → ℝ} (hw₀ : ∀ i ∈ t, 0 ≤ w i)
id                                                 └────┘                               
src                                                └────┘                                 
typ                                                └────┘                               
doc                                                └────┘
741    (hws : 0 < t.sum w) {z : ι → E} (hz : ∀ i ∈ t, z i ∈ s) :
id               └──┘                             
src               └──┘                                   
typ              └──┘                             
742    t.center_mass w z ∈ convex_hull s :=
id     └──────────┘    └─────────┘ 
src     └──────────┘      └─────────┘
typ    └──────────┘    └─────────┘ 
doc     └──────────┘       └─────────┘
743  (convex_convex_hull s).center_mass_mem hw₀ hws (λ i hi, subset_convex_hull s $ hz i hi)
id    └────────────────┘  └─────────────┘  └─┘ └─┘     └┘  └────────────────┘    └┘  └┘
src   └────────────────┘   └─────────────┘                   └────────────────┘
typ   └────────────────┘  └─────────────┘  └─┘ └─┘     └┘  └────────────────┘    └┘  └┘
doc                        └─────────────┘
744  
745  -- TODO : Do we need other versions of the next lemma?
746  
747  /-- Convex hull of `s` is equal to the set of all centers of masses of `finset`s `t`, `z '' t ⊆ s`.
748  This version allows finsets in any type in any universe. -/
749  lemma convex_hull_eq (s : set E) :
id                             └─┘ 
src                            └─┘
typ                            └─┘ 
750    convex_hull s = {x : E | ∃ (ι : Type u') (t : finset ι) (w : ι → ℝ) (z : ι → E)
id     └─────────┘                └──┘          └────┘                   
src    └─────────┘                                └────┘             
typ    └─────────┘                └──┘          └────┘                   
doc    └─────────┘                                   └────┘
751      (hw₀ : ∀ i ∈ t, 0 ≤ w i) (hw₁ : t.sum w = 1) (hz : ∀ i ∈ t, z i ∈ s) , t.center_mass w z = x} :=
id                                  └──┘                         └──────────┘    
src                                      └──┘                                └──────────┘     
typ                                 └──┘                         └──────────┘    
doc                                                                              └──────────┘
752  begin
st   └─────
753    refine subset.antisymm (convex_hull_min _ _) _,
id            └─────────────┘  └─────────────┘
src    └─────┘└─────────────┘ └─────────────┘└─────┘
typ    └─────┘└─────────────┘ └─────────────┘└─────┘
doc    └─────┘                               └─────┘
txt    └─────┘                               └─────┘
par    └─────┘                               └─────┘
pid                                         └─────┘
st   ───────────────────────────────────────────────┘└─
754    { intros x hx,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid            └───┘
st   ───┘└─────────┘└─
755      use [punit, finset.singleton punit.star, λ _, 1, λ _, x, λ _ _, zero_le_one,
id            └───┘  └──────────────┘ └────────┘                        └─────────┘
src      └───┘└───┘└┘└──────────────┘└────────┘└┘ └─────┘ └──┘ └┘ └────┘└─────────┘└─
typ      └───┘└───┘└┘└──────────────┘└────────┘└┘ └─────┘ └──┘└┘ └────┘└─────────┘└─
doc      └───┘     └┘└──────────────┘          └┘ └─────┘ └──┘ └┘ └────┘           └─
txt      └───┘     └┘                          └┘ └─────┘ └──┘ └┘ └────┘           └─
par      └───┘     └┘                          └┘ └─────┘ └──┘ └┘ └────┘           └─
pid         └┘     └┘                          └┘ └─────┘ └──┘ └┘ └────┘           └─
st   ─────────────────────────────────────────────────────────────────────────────────
756        finset.sum_singleton, λ _ _, hx],
id         └──────────────────┘         └┘
src  ─────┘└──────────────────┘└┘ └────┘  
typ  ─────┘└──────────────────┘└┘ └────┘└┘
doc  ─────┘                    └┘ └────┘  
txt  ─────┘                    └┘ └────┘  
par  ─────┘                    └┘ └────┘  
pid  ─────┘                    └┘ └────┘  
st   ─────────────────────────────────────┘└─
757      simp only [finset.center_mass, finset.sum_singleton, inv_one, one_smul] },
id                  └────────────────┘  └──────────────────┘  └─────┘  └──────┘
src      └─────────┘└────────────────┘└┘└──────────────────┘└┘└─────┘└┘└──────┘└┘
typ      └─────────┘└────────────────┘└┘└──────────────────┘└┘└─────┘└┘└──────┘└┘
doc      └─────────┘└────────────────┘└┘                    └┘       └┘        └┘
txt      └─────────┘                  └┘                    └┘       └┘        └┘
par      └─────────┘                  └┘                    └┘       └┘        └┘
pid          └──┘└┘                  └┘                    └┘       └┘        
st   ───────────────────────────────────────────────────────────────────────────┘└┘
758    { rintros x y ⟨ι, sx, wx, zx, hwx₀, hwx₁, hzx, rfl⟩ ⟨ι', sy, wy, zy, hwy₀, hwy₁, hzy, rfl⟩
src      └────────────────────────────────────────────────────────────────────────────────────────
typ      └────────────────────────────────────────────────────────────────────────────────────────
doc      └────────────────────────────────────────────────────────────────────────────────────────
txt      └────────────────────────────────────────────────────────────────────────────────────────
par      └────────────────────────────────────────────────────────────────────────────────────────
pid             └─────────────────────────────────────────────────────────────────────────────────
st   ───┘└────────────────────────────────────────────────────────────────────────────────────────
759        a b ha hb hab,
src  ──────────────────┘
typ  ──────────────────┘
doc  ──────────────────┘
txt  ──────────────────┘
par  ──────────────────┘
pid  ──────────────────┘
st   ──────────────────┘└─
760      rw [finset.center_mass_segment' _ _ _ _ _ _ hwx₁ hwy₁ _ _ hab],
id           └─────────────────────────┘             └──┘ └──┘     └─┘
src      └──┘└─────────────────────────┘└───────────┘        └───┘   
typ      └──┘└─────────────────────────┘└───────────┘└──┘└──┘└───┘└─┘
doc      └──┘└─────────────────────────┘└───────────┘        └───┘   
txt      └──┘                           └───────────┘        └───┘   
par      └──┘                           └───────────┘        └───┘   
pid        └┘                           └───────────┘        └───┘   
st   ────────────────────────────────────────────────────────────────┘└──
761      refine ⟨_, _, _, _, _, _, _, rfl⟩,
id                                    └─┘
src      └─────┘ └───────────────────┘└─┘
typ      └─────┘ └───────────────────┘└─┘
doc      └─────┘ └───────────────────┘   
txt      └─────┘ └───────────────────┘   
par      └─────┘ └───────────────────┘   
pid             └───────────────────┘   
st   ────────────────────────────────────┘└─
762      { rintros i hi,
src        └──────────┘
typ        └──────────┘
doc        └──────────┘
txt        └──────────┘
par        └──────────┘
pid               └───┘
st   ─────┘└──────────┘└─
763        rw [finset.mem_union, finset.mem_image, finset.mem_image] at hi,
id             └──────────────┘  └──────────────┘  └──────────────┘
src        └──┘└──────────────┘└┘└──────────────┘└┘└──────────────┘└─────┘
typ        └──┘└──────────────┘└┘└──────────────┘└┘└──────────────┘└─────┘
doc        └──┘                └┘                └┘                └─────┘
txt        └──┘                └┘                └┘                └─────┘
par        └──┘                └┘                └┘                └─────┘
pid          └┘                └┘                └┘                └────┘
st   ─────────────────────────┘└────────────────┘└────────────────┘└────┘└─
764        rcases hi with ⟨j, hj, rfl⟩|⟨j, hj, rfl⟩;
id                └┘
src        └─────┘  └─────────────────────────────┘
typ        └─────┘└┘└─────────────────────────────┘
doc        └─────┘  └─────────────────────────────┘
txt        └─────┘  └─────────────────────────────┘
par        └─────┘  └─────────────────────────────┘
pid                └─────────────────────────────┘
st   ────────────────────────────────────────────────
765          simp only [sum.elim_inl, sum.elim_inr];
id                      └──────────┘  └──────────┘
src          └─────────┘└──────────┘└┘└──────────┘
typ          └─────────┘└──────────┘└┘└──────────┘
doc          └─────────┘            └┘            
txt          └─────────┘            └┘            
par          └─────────┘            └┘            
pid              └──┘└┘            └┘            
st   ────────────────────────────────────────────────
766          apply_rules [mul_nonneg, hwx₀, hwy₀] },
id                        └────────┘
src          └───────────┘└────────┘└┘    └┘    └┘
typ          └───────────┘└────────┘└┘    └┘    └┘
doc          └───────────┘          └┘    └┘    └┘
txt          └───────────┘          └┘    └┘    └┘
par          └───────────┘          └┘    └┘    └┘
pid                     └┘          └┘    └┘    
st   ────────────────────────────────────────────┘└┘
767      { simp [finset.sum_sum_elim, finset.mul_sum.symm, *] },
id               └─────────────────┘
src        └────┘└─────────────────┘└┘                   └───┘
typ        └────┘└─────────────────┘└┘└─────────────────┘└───┘
doc        └────┘                   └┘                   └───┘
txt        └────┘                   └┘                   └───┘
par        └────┘                   └┘                   └───┘
pid                               └┘                   └──┘
st   ─────┘└─────────────────────────────────────────────────┘└┘
768      { intros i hi,
src        └─────────┘
typ        └─────────┘
doc        └─────────┘
txt        └─────────┘
par        └─────────┘
pid              └───┘
st   ────────────────┘└─
769        rw [finset.mem_union, finset.mem_image, finset.mem_image] at hi,
id             └──────────────┘  └──────────────┘  └──────────────┘
src        └──┘└──────────────┘└┘└──────────────┘└┘└──────────────┘└─────┘
typ        └──┘└──────────────┘└┘└──────────────┘└┘└──────────────┘└─────┘
doc        └──┘                └┘                └┘                └─────┘
txt        └──┘                └┘                └┘                └─────┘
par        └──┘                └┘                └┘                └─────┘
pid          └┘                └┘                └┘                └────┘
st   ─────────────────────────┘└────────────────┘└────────────────┘└────┘└─
770        rcases hi with ⟨j, hj, rfl⟩|⟨j, hj, rfl⟩;
id                └┘
src        └─────┘  └─────────────────────────────┘
typ        └─────┘└┘└─────────────────────────────┘
doc        └─────┘  └─────────────────────────────┘
txt        └─────┘  └─────────────────────────────┘
par        └─────┘  └─────────────────────────────┘
pid                └─────────────────────────────┘
st   ────────────────────────────────────────────────
771          simp only [sum.elim_inl, sum.elim_inr]; apply_rules [hzx, hzy] } },
id                      └──────────┘  └──────────┘
src          └─────────┘└──────────┘└┘└──────────┘  └───────────┘   └┘   └┘
typ          └─────────┘└──────────┘└┘└──────────┘  └───────────┘   └┘   └┘
doc          └─────────┘            └┘              └───────────┘   └┘   └┘
txt          └─────────┘            └┘              └───────────┘   └┘   └┘
par          └─────────┘            └┘              └───────────┘   └┘   └┘
pid              └──┘└┘            └┘                         └┘   └┘   
st   ──────────────────────────────────────────────────────────────────────┘└──┘
772    { rintros _ ⟨ι, t, w, z, hw₀, hw₁, hz, rfl⟩,
src      └───────────────────────────────────────┘
typ      └───────────────────────────────────────┘
doc      └───────────────────────────────────────┘
txt      └───────────────────────────────────────┘
par      └───────────────────────────────────────┘
pid             └────────────────────────────────┘
st   ────────────────────────────────────────────┘└─
773      exact t.center_mass_mem_convex_hull hw₀ (hw₁.symm ▸ zero_lt_one) hz }
id             └───────────────────────────┘ └─┘  └──────┘  └─────────┘  └┘
src      └────┘└───────────────────────────┘    └──────┘└─────────┘└┘  
typ      └────┘└───────────────────────────┘└─┘ └──────┘└─────────┘└┘└┘
doc      └────┘                                                     └┘  
txt      └────┘                                                     └┘  
par      └────┘                                                     └┘  
pid                                                                └┘  
st   ───────────────────────────────────────────────────────────────────────┘└─
774  end
st   ──┘
775  
776  /-- Maximum principle for convex functions. If a function `f` is convex on the convex hull of `s`,
777  then `f` can't have a maximum on `convex_hull s` outside of `s`. -/
778  lemma convex_on.exists_ge_of_mem_convex_hull {f : E → ℝ} (hf : convex_on (convex_hull s) f)
id                                                                └───────┘  └─────────┘   
src                                                                └───────┘  └─────────┘
typ                                                               └───────┘  └─────────┘   
doc                                                                 └───────┘  └─────────┘
779    {x} (hx : x ∈ convex_hull s) : ∃ y ∈ s, f x ≤ f y :=
id                 └─────────┘              
src                 └─────────┘                 
typ                └─────────┘              
doc                  └─────────┘
780  begin
st   └─────
781    rw convex_hull_eq at hx,
id        └────────────┘
src    └─┘└────────────┘└────┘
typ    └─┘└────────────┘└────┘
doc    └─┘└────────────┘└────┘
txt    └─┘              └────┘
par    └─┘              └────┘
pid                    └────┘
st   ────────────────────────┘└─
782    rcases hx with ⟨α, t, w, z, hw₀, hw₁, hz, rfl⟩,
id            └┘
src    └─────┘  └───────────────────────────────────┘
typ    └─────┘└┘└───────────────────────────────────┘
doc    └─────┘  └───────────────────────────────────┘
txt    └─────┘  └───────────────────────────────────┘
par    └─────┘  └───────────────────────────────────┘
pid            └───────────────────────────────────┘
st   ───────────────────────────────────────────────┘└─
783    rcases hf.exists_ge_of_center_mass hw₀ (hw₁.symm ▸ zero_lt_one)
id            └─────────────────────────┘ └─┘  └──────┘  └─────────┘
src    └─────┘└─────────────────────────┘    └──────┘└─────────┘└─
typ    └─────┘└─────────────────────────┘└─┘ └──────┘└─────────┘└─
doc    └─────┘└─────────────────────────┘                        └─
txt    └─────┘                                                   └─
par    └─────┘                                                   └─
pid                                                             └─
st   ──────────────────────────────────────────────────────────────────
784      (λ i hi, subset_convex_hull s (hz i hi)) with ⟨i, hit, Hi⟩,
id                └────────────────┘   └┘
src  ───┘  └─────┘└────────────────┘       └──────────────────┘
typ  ───┘  └─────┘└────────────────┘ └┘   └──────────────────┘
doc  ───┘  └─────┘                         └──────────────────┘
txt  ───┘  └─────┘                         └──────────────────┘
par  ───┘  └─────┘                         └──────────────────┘
pid  ───┘  └─────┘                         └──────────────────┘
st   ─────────────────────────────────────────────────────────────┘└─
785    exact ⟨z i, hz i hit, Hi⟩
id                └┘  └─┘  └┘
src    └────┘   └┘      └┘  └┘
typ    └────┘  └┘└┘└─┘└┘└┘└┘
doc    └────┘   └┘      └┘  └┘
txt    └────┘   └┘      └┘  └┘
par    └────┘   └┘      └┘  └┘
pid            └┘      └┘  
st   ───────────────────────────┘
786  end
st   └─┘
787  
788  lemma set.finite.convex_hull_eq {s : set E} (hs : finite s) :
id                                        └─┘         └────┘ 
src                                       └─┘          └────┘
typ                                       └─┘         └────┘ 
doc                                                    └────┘
789    convex_hull s = {x : E | ∃ (w : E → ℝ) (hw₀ : ∀ y ∈ s, 0 ≤ w y) (hw₁ : hs.to_finset.sum w = 1),
id     └─────────┘                                               └┘└────────┘└──┘     
src    └─────────┘                                                         └────────┘└──┘      
typ    └─────────┘                                               └┘└────────┘└──┘     
doc    └─────────┘                                                              └────────┘
790      hs.to_finset.center_mass w id = x} :=
id       └┘└────────┘└──────────┘  └┘  
src        └────────┘└──────────┘   └┘ 
typ      └┘└────────┘└──────────┘  └┘  
doc        └────────┘└──────────┘
791  begin
st   └─────
792    refine subset.antisymm (convex_hull_min _ _) _,
id            └─────────────┘  └─────────────┘
src    └─────┘└─────────────┘ └─────────────┘└─────┘
typ    └─────┘└─────────────┘ └─────────────┘└─────┘
doc    └─────┘                               └─────┘
txt    └─────┘                               └─────┘
par    └─────┘                               └─────┘
pid                                         └─────┘
st   ───────────────────────────────────────────────┘└─
793    { intros x hx,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid            └───┘
st   ───┘└─────────┘└─
794      replace hx : x ∈ hs.to_finset, from finite.mem_to_finset.2 hx,
id                      └──────────┘       └──────────────────┘   └┘
src      └───────────┘ └──────────┘  └───┘└──────────────────┘└─┘
typ      └───────────┘└──────────┘  └───┘└──────────────────┘└─┘└┘
doc      └───────────┘  └──────────┘  └───┘                    └─┘
txt      └───────────┘                └───┘                    └─┘
par      └───────────┘                └───┘                    └─┘
pid             └─┘└─┘                └───┘                    └─┘
st   ────────────────────────────────┘└──────────────────────────────┘└─
795      refine ⟨_, _, _, finset.center_mass_ite_eq _ _ _ hx⟩,
id                        └───────────────────────┘       └┘
src      └─────┘ └───────┘└───────────────────────┘└─────┘  
typ      └─────┘ └───────┘└───────────────────────┘└─────┘└┘
doc      └─────┘ └───────┘                         └─────┘  
txt      └─────┘ └───────┘                         └─────┘  
par      └─────┘ └───────┘                         └─────┘  
pid             └───────┘                         └─────┘  
st   ───────────────────────────────────────────────────────┘└─
796      { intros, split_ifs, exacts [zero_le_one, le_refl 0] },
id                                    └─────────┘  └─────┘
src        └────┘  └───────┘  └──────┘└─────────┘└┘└─────┘└──┘
typ        └────┘  └───────┘  └──────┘└─────────┘└┘└─────┘└──┘
doc        └────┘  └───────┘  └──────┘           └┘       └──┘
txt        └────┘  └───────┘  └──────┘           └┘       └──┘
par        └────┘  └───────┘  └──────┘           └┘       └──┘
pid                                 └┘           └┘       └─┘
st   ─────┘└────┘└─────────┘└────────────────────────────────┘└┘
797      { rw [finset.sum_ite_eq, if_pos hx] } },
id             └───────────────┘  └────┘ └┘
src        └──┘└───────────────┘└┘└────┘  └┘
typ        └──┘└───────────────┘└┘└────┘└┘└┘
doc        └──┘                 └┘        └┘
txt        └──┘                 └┘        └┘
par        └──┘                 └┘        └┘
pid          └┘                 └┘        
st   ──────────────────────────┘└─────────┘└──┘
798    { rintros x y ⟨wx, hwx₀, hwx₁, rfl⟩ ⟨wy, hwy₀, hwy₁, rfl⟩
src      └───────────────────────────────────────────────────────
typ      └───────────────────────────────────────────────────────
doc      └───────────────────────────────────────────────────────
txt      └───────────────────────────────────────────────────────
par      └───────────────────────────────────────────────────────
pid             └────────────────────────────────────────────────
st   ───┘└───────────────────────────────────────────────────────
799        a b ha hb hab,
src  ──────────────────┘
typ  ──────────────────┘
doc  ──────────────────┘
txt  ──────────────────┘
par  ──────────────────┘
pid  ──────────────────┘
st   ──────────────────┘└─
800      rw [finset.center_mass_segment _ _ _ _ hwx₁ hwy₁ _ _ hab],
id           └────────────────────────┘         └──┘ └──┘     └─┘
src      └──┘└────────────────────────┘└───────┘        └───┘   
typ      └──┘└────────────────────────┘└───────┘└──┘└──┘└───┘└─┘
doc      └──┘└────────────────────────┘└───────┘        └───┘   
txt      └──┘                          └───────┘        └───┘   
par      └──┘                          └───────┘        └───┘   
pid        └┘                          └───────┘        └───┘   
st   ───────────────────────────────────────────────────────────┘└──
801      refine ⟨_, _, _, rfl⟩,
id                        └─┘
src      └─────┘ └───────┘└─┘
typ      └─────┘ └───────┘└─┘
doc      └─────┘ └───────┘   
txt      └─────┘ └───────┘   
par      └─────┘ └───────┘   
pid             └───────┘   
st   ────────────────────────┘└─
802      { rintros i hi,
src        └──────────┘
typ        └──────────┘
doc        └──────────┘
txt        └──────────┘
par        └──────────┘
pid               └───┘
st   ─────┘└──────────┘└─
803        apply_rules [add_nonneg, mul_nonneg, hwx₀, hwy₀], },
id                      └────────┘  └────────┘
src        └───────────┘└────────┘└┘└────────┘└┘    └┘    
typ        └───────────┘└────────┘└┘└────────┘└┘    └┘    
doc        └───────────┘          └┘          └┘    └┘    
txt        └───────────┘          └┘          └┘    └┘    
par        └───────────┘          └┘          └┘    └┘    
pid                   └┘          └┘          └┘    └┘    
st   ─────────────────────────────────────────────────────┘└──┘
804      { simp only [finset.sum_add_distrib, finset.mul_sum.symm, mul_one, *] } },
id                    └────────────────────┘                       └─────┘
src        └─────────┘└────────────────────┘└┘                   └┘└─────┘└───┘
typ        └─────────┘└────────────────────┘└┘└─────────────────┘└┘└─────┘└───┘
doc        └─────────┘                      └┘                   └┘       └───┘
txt        └─────────┘                      └┘                   └┘       └───┘
par        └─────────┘                      └┘                   └┘       └───┘
pid            └──┘└┘                      └┘                   └┘       └──┘
st   ─────────────────────────────────────────────────────────────────────────┘└──┘
805    { rintros _ ⟨w, hw₀, hw₁, rfl⟩,
src      └──────────────────────────┘
typ      └──────────────────────────┘
doc      └──────────────────────────┘
txt      └──────────────────────────┘
par      └──────────────────────────┘
pid             └───────────────────┘
st   ───────────────────────────────┘└─
806      exact hs.to_finset.center_mass_mem_convex_hull (λ x hx, hw₀ _ $ finite.mem_to_finset.1 hx)
id             └──────────────────────────────────────┘          └─┘
src      └────┘└──────────────────────────────────────┘  └─────┘   └─┘                     └─┘  └─
typ      └────┘└──────────────────────────────────────┘  └─────┘└─┘└─┘                     └─┘  └─
doc      └────┘└──────────────────────────────────────┘  └─────┘   └─┘                     └─┘  └─
txt      └────┘                                          └─────┘   └─┘                     └─┘  └─
par      └────┘                                          └─────┘   └─┘                     └─┘  └─
pid                                                     └─────┘   └─┘                     └─┘  └─
st   ───────────────────────────────────────────────────────────────────────────────────────────────
807        (hw₁.symm ▸ zero_lt_one) (λ x hx, finite.mem_to_finset.1 hx) }
id          └──────┘  └─────────┘           └──────────────────┘
src  ─────┘ └──────┘└─────────┘└┘  └─────┘└──────────────────┘└─┘  └┘
typ  ─────┘ └──────┘└─────────┘└┘  └─────┘└──────────────────┘└─┘  └┘
doc  ─────┘                     └┘  └─────┘                    └─┘  └┘
txt  ─────┘                     └┘  └─────┘                    └─┘  └┘
par  ─────┘                     └┘  └─────┘                    └─┘  └┘
pid  ─────┘                     └┘  └─────┘                    └─┘  
st   ──────────────────────────────────────────────────────────────────┘└─
808  end
st   ──┘
809  
810  lemma is_linear_map.convex_hull_image {f : E → F} (hf : is_linear_map ℝ f) (s : set E) :
id                                                         └───────────┘         └─┘ 
src                                                          └───────────┘          └─┘
typ                                                        └───────────┘         └─┘ 
811    convex_hull (f '' s) = f '' convex_hull s :=
id     └─────────┘   └┘     └┘ └─────────┘ 
src    └─────────┘    └┘       └┘ └─────────┘
typ    └─────────┘   └┘     └┘ └─────────┘ 
doc    └─────────┘                 └─────────┘
812  set.subset.antisymm (convex_hull_min (image_subset _ (subset_convex_hull s)) $
id   └─────────────────┘  └─────────────┘  └──────────┘    └────────────────┘ 
src  └─────────────────┘  └─────────────┘  └──────────┘    └────────────────┘
typ  └─────────────────┘  └─────────────┘  └──────────┘    └────────────────┘ 
813    (convex_convex_hull s).is_linear_image hf)
id      └────────────────┘  └─────────────┘  └┘
src     └────────────────┘   └─────────────┘
typ     └────────────────┘  └─────────────┘  └┘
814    (image_subset_iff.2 $ convex_hull_min
id      └──────────────┘    └─────────────┘
src     └──────────────┘    └─────────────┘
typ     └──────────────┘    └─────────────┘
doc     └──────────────┘
815      (image_subset_iff.1 $ subset_convex_hull _)
id        └──────────────┘    └────────────────┘
src       └──────────────┘    └────────────────┘
typ       └──────────────┘    └────────────────┘
doc       └──────────────┘
816      ((convex_convex_hull _).is_linear_preimage hf))
id         └────────────────┘   └────────────────┘  └┘
src        └────────────────┘   └────────────────┘
typ        └────────────────┘   └────────────────┘  └┘
817  
818  lemma linear_map.convex_hull_image (f : E →ₗ[ℝ] F) (s : set E) :
id                                            └─┘        └─┘ 
src                                            └─┘         └─┘
typ                                           └─┘        └─┘ 
819    convex_hull (f '' s) = f '' convex_hull s :=
id     └─────────┘   └┘     └┘ └─────────┘ 
src    └─────────┘    └┘       └┘ └─────────┘
typ    └─────────┘   └┘     └┘ └─────────┘ 
doc    └─────────┘                 └─────────┘
820  f.is_linear.convex_hull_image s
id   └────────┘└────────────────┘ 
src   └────────┘└────────────────┘
typ  └────────┘└────────────────┘ 
821  
822  end convex_hull
823  
824  /-! ### Simplex -/
825  
826  section simplex
827  
828  variables (ι) [fintype ι] {f : ι → ℝ}
id                  └─────┘             
src                 └─────┘             
typ                 └─────┘             
doc                 └─────┘
829  
830  /-- Standard simplex in the space of functions `ι → ℝ` is the set
831  of vectors with non-negative coordinates with total sum `1`. -/
832  def std_simplex (ι : Type*) [fintype ι] : set (ι → ℝ) :=
id                                └─────┘     └─┘     
src                               └─────┘      └─┘      
typ                               └─────┘     └─┘     
doc                               └─────┘
833  { f | (∀ x, 0 ≤ f x) ∧ finset.univ.sum f = 1 }
id                   └─────────┘└──┘  
src                      └─────────┘└──┘   
typ                  └─────────┘└──┘  
doc                         └─────────┘
834  
835  lemma std_simplex_eq_inter :
836    std_simplex ι = (⋂ x, {f | 0 ≤ f x}) ∩ {f | finset.univ.sum f = 1} :=
id     └─────────┘                    └─────────┘└──┘  
src    └─────────┘                          └─────────┘└──┘   
typ    └─────────┘                    └─────────┘└──┘  
doc    └─────────┘                               └─────────┘
837  by { ext f, simp only [std_simplex, set.mem_inter_eq, set.mem_Inter, set.mem_set_of_eq] }
id                          └─────────┘  └──────────────┘  └───────────┘  └───────────────┘
src       └───┘  └─────────┘└─────────┘└┘└──────────────┘└┘└───────────┘└┘└───────────────┘└┘
typ       └───┘  └─────────┘└─────────┘└┘└──────────────┘└┘└───────────┘└┘└───────────────┘└┘
doc       └───┘  └─────────┘└─────────┘└┘                └┘             └┘                 └┘
txt       └───┘  └─────────┘           └┘                └┘             └┘                 └┘
par       └───┘  └─────────┘           └┘                └┘             └┘                 └┘
pid          └┘      └──┘└┘           └┘                └┘             └┘                 
st     └──────┘└────────────────────────────────────────────────────────────────────────────┘└┘
838  
839  lemma convex_std_simplex : convex (std_simplex ι) :=
id                              └────┘  └─────────┘ 
src                             └────┘  └─────────┘
typ                             └────┘  └─────────┘ 
doc                             └────┘  └─────────┘
840  begin
st   └─────
841    refine λ f g hf hg a b ha hb hab, ⟨λ x, _, _⟩,
src    └─────┘ └────────────────────────┘  └───────┘
typ    └─────┘ └────────────────────────┘  └───────┘
doc    └─────┘ └────────────────────────┘  └───────┘
txt    └─────┘ └────────────────────────┘  └───────┘
par    └─────┘ └────────────────────────┘  └───────┘
pid           └────────────────────────┘  └───────┘
st   ──────────────────────────────────────────────┘└─
842    { apply_rules [add_nonneg, mul_nonneg, hf.1, hg.1] },
id                    └────────┘  └────────┘  └┘    └┘
src      └───────────┘└────────┘└┘└────────┘└┘  └──┘  └──┘
typ      └───────────┘└────────┘└┘└────────┘└┘└┘└──┘└┘└──┘
doc      └───────────┘          └┘          └┘  └──┘  └──┘
txt      └───────────┘          └┘          └┘  └──┘  └──┘
par      └───────────┘          └┘          └┘  └──┘  └──┘
pid                 └┘          └┘          └┘  └──┘  └─┘
st   ───┘└───────────────────────────────────────────────┘└┘
843    { erw [finset.sum_add_distrib, ← finset.smul_sum, ← finset.smul_sum, hf.2, hg.2,
id            └────────────────────┘    └─────────────┘    └─────────────┘  └┘    └┘
src      └───┘└────────────────────┘└──┘└─────────────┘└──┘└─────────────┘└┘  └──┘  └───
typ      └───┘└────────────────────┘└──┘└─────────────┘└──┘└─────────────┘└┘└┘└──┘└┘└───
doc      └───┘                      └──┘               └──┘               └┘  └──┘  └───
txt      └───┘                      └──┘               └──┘               └┘  └──┘  └───
par      └───┘                      └──┘               └──┘               └┘  └──┘  └───
pid         └┘                      └──┘               └──┘               └┘  └──┘  └───
st   ──────────────────────────────┘└─────────────────┘└─────────────────┘└──┘└────┘└───
844        smul_eq_mul, smul_eq_mul, mul_one, mul_one],
id         └─────────┘  └─────────┘  └─────┘  └─────┘
src  ─────┘└─────────┘└┘└─────────┘└┘└─────┘└┘└─────┘
typ  ─────┘└─────────┘└┘└─────────┘└┘└─────┘└┘└─────┘
doc  ─────┘           └┘           └┘       └┘       
txt  ─────┘           └┘           └┘       └┘       
par  ─────┘           └┘           └┘       └┘       
pid  ─────┘           └┘           └┘       └┘       
st   ────────────────┘└───────────┘└───────┘└───────┘└──
845      exact hab }
id             └─┘
src      └────┘   
typ      └────┘└─┘
doc      └────┘   
txt      └────┘   
par      └────┘   
pid              
st   ─────────────┘└─
846  end
st   ──┘
847  
848  variable {ι}
849  
850  lemma ite_eq_mem_std_simplex (i : ι) : (λ j, ite (i = j) (1:ℝ) 0) ∈ std_simplex ι :=
id                                              └─┘               └─────────┘ 
src                                               └─┘                 └─────────┘
typ                                             └─┘               └─────────┘ 
doc                                                                      └─────────┘
851  ⟨λ j, by simp only []; split_ifs; norm_num, by rw [finset.sum_ite_eq, if_pos (finset.mem_univ _)] ⟩
id                                                     └───────────────┘  └────┘  └─────────────┘
src           └──────────┘  └───────┘  └──────┘     └──┘└───────────────┘└┘└────┘ └─────────────┘└───┘
typ          └──────────┘  └───────┘  └──────┘     └──┘└───────────────┘└┘└────┘ └─────────────┘└───┘
doc           └──────────┘  └───────┘  └──────┘     └──┘                 └┘                      └───┘
txt           └──────────┘  └───────┘  └──────┘     └──┘                 └┘                      └───┘
par           └──────────┘  └───────┘  └──────┘     └──┘                 └┘                      └───┘
pid               └──┘└─┘                            └┘                 └┘                      └──┘
st           └────────────────────────────────┘    └────────────────────┘└──────────────────────────┘
852  
853  /-- `std_simplex ι` is the convex hull of the canonical basis in `ι → ℝ`. -/
854  lemma convex_hull_basis_eq_std_simplex :
855    convex_hull (range $ λ(i j:ι), if i = j then (1:ℝ) else 0) = std_simplex ι :=
id     └─────────┘  └───┘                                     └─────────┘ 
src    └─────────┘  └───┘                                        └─────────┘
typ    └─────────┘  └───┘                                     └─────────┘ 
doc    └─────────┘  └───┘                                           └─────────┘
856  begin
st   └─────
857    refine subset.antisymm (convex_hull_min _ (convex_std_simplex ι)) _,
id            └─────────────┘  └─────────────┘    └────────────────┘ 
src    └─────┘└─────────────┘ └─────────────┘└─┘ └────────────────┘ └──┘
typ    └─────┘└─────────────┘ └─────────────┘└─┘ └────────────────┘└──┘
doc    └─────┘                               └─┘                    └──┘
txt    └─────┘                               └─┘                    └──┘
par    └─────┘                               └─┘                    └──┘
pid                                         └─┘                    └──┘
st   ────────────────────────────────────────────────────────────────────┘└─
858    { rintros _ ⟨i, rfl⟩,
src      └────────────────┘
typ      └────────────────┘
doc      └────────────────┘
txt      └────────────────┘
par      └────────────────┘
pid             └─────────┘
st   ───┘└────────────────┘└─
859      exact ite_eq_mem_std_simplex i },
id             └────────────────────┘ 
src      └────┘└────────────────────┘ 
typ      └────┘└────────────────────┘
doc      └────┘                       
txt      └────┘                       
par      └────┘                       
pid                                  
st   ──────────────────────────────────┘└┘
860    { rintros w ⟨hw₀, hw₁⟩,
src      └──────────────────┘
typ      └──────────────────┘
doc      └──────────────────┘
txt      └──────────────────┘
par      └──────────────────┘
pid             └───────────┘
st   ───────────────────────┘└─
861      rw [pi_eq_sum_univ w, ← finset.univ.center_mass_eq_of_sum_1 _ hw₁],
id           └────────────┘     └─────────────────────────────────┘   └─┘
src      └──┘└────────────┘ └──┘└─────────────────────────────────┘└─┘   
typ      └──┘└────────────┘└──┘└─────────────────────────────────┘└─┘└─┘
doc      └──┘└────────────┘ └──┘└─────────────────────────────────┘└─┘   
txt      └──┘               └──┘                                   └─┘   
par      └──┘               └──┘                                   └─┘   
pid        └┘               └──┘                                   └─┘   
st   ───────────────────────┘└───────────────────────────────────────────┘└──
862      exact finset.univ.center_mass_mem_convex_hull (λ i hi, hw₀ i)
id             └─────────────────────────────────────┘          └─┘
src      └────┘└─────────────────────────────────────┘  └─────┘    └─
typ      └────┘└─────────────────────────────────────┘  └─────┘└─┘ └─
doc      └────┘└─────────────────────────────────────┘  └─────┘    └─
txt      └────┘                                         └─────┘    └─
par      └────┘                                         └─────┘    └─
pid                                                    └─────┘    └─
st   ──────────────────────────────────────────────────────────────────
863        (hw₁.symm ▸ zero_lt_one) (λ i hi, mem_range_self i) }
id          └──────┘  └─────────┘           └────────────┘
src  ─────┘ └──────┘└─────────┘└┘  └─────┘└────────────┘ └┘
typ  ─────┘ └──────┘└─────────┘└┘  └─────┘└────────────┘ └┘
doc  ─────┘                     └┘  └─────┘               └┘
txt  ─────┘                     └┘  └─────┘               └┘
par  ─────┘                     └┘  └─────┘               └┘
pid  ─────┘                     └┘  └─────┘               
st   ─────────────────────────────────────────────────────────┘└─
864  end
st   ──┘
865  
866  variable {ι}
867  
868  /-- Convex hull of a finite set is the image of the standard simplex in `s → ℝ`
869  under the linear map sending each function `w` to `s.sum (λ x, w x • x)`.
870  
871  Since we have no sums over finite sets, we use sum over `@finset.univ _ hs.fintype`.
872  The map is defined in terms of operations on `(s → ℝ) →ₗ[ℝ] ℝ` so that later we will not need
873  to prove that this map is linear. -/
874  lemma set.finite.convex_hull_eq_image {s : set E} (hs : finite s) :
id                                              └─┘         └────┘ 
src                                             └─┘          └────┘
typ                                             └─┘         └────┘ 
doc                                                          └────┘
875    convex_hull s =
id     └─────────┘  
src    └─────────┘   
typ    └─────────┘  
doc    └─────────┘
876      (⇑((@finset.univ _ hs.fintype).sum (λ x, (linear_map.proj x : (s → ℝ) →ₗ[ℝ] ℝ).smul_right x.1))) ''
id           └─────────┘   └┘└──────┘ └─┘        └─────────────┘          └─┘  └────────┘       └┘
src          └─────────┘     └──────┘ └─┘         └─────────────┘            └─┘  └────────┘        └┘
typ          └─────────┘   └┘└──────┘ └─┘        └─────────────┘          └─┘  └────────┘       └┘
doc           └─────────┘     └──────┘             └─────────────┘                     └────────┘
877        (@std_simplex _ hs.fintype) :=
id           └─────────┘   └┘└──────┘
src          └─────────┘     └──────┘
typ          └─────────┘   └┘└──────┘
doc          └─────────┘     └──────┘
878  begin
st   └─────
879    rw [← convex_hull_basis_eq_std_simplex, ← linear_map.convex_hull_image, ← range_comp, (∘)],
id           └──────────────────────────────┘    └──────────────────────────┘    └────────┘  
src    └────┘└──────────────────────────────┘└──┘└──────────────────────────┘└──┘└────────┘└┘└─┘
typ    └────┘└──────────────────────────────┘└──┘└──────────────────────────┘└──┘└────────┘└┘└─┘
doc    └────┘└──────────────────────────────┘└──┘                            └──┘          └┘ └─┘
txt    └────┘                                └──┘                            └──┘          └┘ └─┘
par    └────┘                                └──┘                            └──┘          └┘ └─┘
pid      └──┘                                └──┘                            └──┘          └┘ └─┘
st   ───────────────────────────────────────┘└──────────────────────────────┘└────────────┘└───┘└──
880    apply congr_arg,
id           └───────┘
src    └────┘└───────┘
typ    └────┘└───────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ────────────────┘└─
881    convert (subtype.range_val s).symm,
id              └───────────────┘ 
src    └──────┘ └───────────────┘ └────┘
typ    └──────┘ └───────────────┘└────┘
doc    └──────┘                   └────┘
txt    └──────┘                   └────┘
par    └──────┘                   └────┘
pid                              └───┘
st   ───────────────────────────────────┘└─
882    ext x,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid       └┘
st   ──────┘└─
883    simp [linear_map.sum_apply, ite_smul, finset.sum_ite _ _ (λ x, x), finset.filter_eq]
id           └──────────────────┘  └──────┘  └────────────┘               └──────────────┘
src    └────┘└──────────────────┘└┘└──────┘└┘└────────────┘└───┘  └──┘ └─┘└──────────────┘└┘
typ    └────┘└──────────────────┘└┘└──────┘└┘└────────────┘└───┘  └──┘ └─┘└──────────────┘└┘
doc    └────┘                    └┘        └┘              └───┘  └──┘ └─┘└──────────────┘└┘
txt    └────┘                    └┘        └┘              └───┘  └──┘ └─┘                └┘
par    └────┘                    └┘        └┘              └───┘  └──┘ └─┘                └┘
pid                            └┘        └┘              └───┘  └──┘ └─┘                
st   ──────────────────────────────────────────────────────────────────────────────────────┘
884  end
st   └─┘
885  
886  /-- All values of a function `f ∈ std_simplex ι` belong to `[0, 1]`. -/
887  lemma mem_Icc_of_mem_std_simplex (hf : f ∈ std_simplex ι) (x) :
id                                            └─────────┘ 
src                                            └─────────┘
typ                                           └─────────┘ 
doc                                             └─────────┘
888    f x ∈ I :=
id        
src         
typ       
doc          
889  ⟨hf.1 x, hf.2 ▸ finset.single_le_sum (λ y hy, hf.1 y) (finset.mem_univ x)⟩
id    └┘    └┘   └──────────────────┘     └┘  └┘     └─────────────┘ 
src               └──────────────────┘                  └─────────────┘
typ   └┘    └┘   └──────────────────┘     └┘  └┘     └─────────────┘ 
890  
891  end simplex